RESEARCH ARTICLE


A Formal Model of Requirements



Francois Defossez*, 1, 2, Simon Collart-Dutilleul1, 3, Philippe Bon1, 2
1 Univ Nord de France, F-59000 Lille, France
2 INRETS/ESTAS, 20 rue Élisée Reclus BP 317 59666 Villeneuve d’Ascq CEDEX, France
3 École Centrale de Lille/LAGIS, Cité scientifique BP 48 59651 Villeneuve d’Ascq, France


Article Metrics

CrossRef Citations:
0
Total Statistics:

Full-Text HTML Views: 214
Abstract HTML Views: 462
PDF Downloads: 154
Total Views/Downloads: 830
Unique Statistics:

Full-Text HTML Views: 164
Abstract HTML Views: 336
PDF Downloads: 118
Total Views/Downloads: 618



© 2011 Defossezet al;

open-access license: This is an open access article distributed under the terms of the Creative Commons Attribution 4.0 International Public License (CC-BY 4.0), a copy of which is available at: https://creativecommons.org/licenses/by/4.0/legalcode. This license permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.

* Address correspondence to this author at the INRETS/ESTAS, 20 rue Elisee Reclus BP 317 59666 Villeneuve d'Ascq CEDEX, France; Tel: + 33320438407; E-mail: françois.defossez@inrets.fr


Abstract

This paper introduces a methodology to analyze the safety of timed discrete event systems. Our case-study is the level crossing, a critical component for the safety of railway systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we describe a process identified as a solution for the system functioning. This method consists in exploring all the possible behaviors of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the model of requirements previously built.

Keywords: Temporal and safety requirements, requirement engineering, traceability, modelling, Petri net, Railway transport, level crossing, .