Scenario-based system design with colored Petri nets: an application to train control systems

For the goal of model-based system software development, this paper exploits the formalism of colored Petri nets (CPNs) to design complex systems based on scenarios. The specification of UML sequence diagrams which are easily understood by customers, requirement engineers and software developers are adopted to represent scenarios as specification models. A scenario is a partial description of the system behavior, describing how users, system components and the environment interact. Thus scenarios need to be synthesized in order to obtain an overall system behavior. A large number of works (e.g., Whittle and Schumann in Proceedings of the 2000 international conference on software engineering, pp 314–323, 2000 ; Elkoutbi and Keller in Application and theory of Petri nets, 2000 ; Damas et al. in Proceedings of the 14th ACM SIGSOFT international symposium on foundations of software engineering, pp 197–207, 2000 ; Uchitel et al. in IEEE Trans Softw Eng 29(2):99–115, 2003 ) have investigated scenario synthesis providing approaches or algorithms. These synthesis approaches and algorithms result in either Petri net models (e.g., Elkoutbi and Keller 2000 ; Ameedeen and Bordbar in 12th international IEEE enterprise distributed object computing conference (EDOC), pp 213–221, 2008 ) that are mainly suitable for scenario validation or other forms of behavior models (e.g., labeled transition systems in Damas et al. 2000 ; Uchitel et al. 2003 and statecharts in Krüger et al. in Distributed and parallel embedded systems, pp 61–71, 1999 ; Whittle et al. 2000 ) that may be regarded as design models. Petri nets are well known for describing distributed and concurrent complex systems. Furthermore, numerous techniques, e.g., simulation, testing, state space-based techniques, structural methods and model checking, are currently available for analyzing Petri net models. Therefore, design models in the form of Petri nets, integrating all scenarios into a coherent whole and fitting for further detailed design, are promising. To this end, we present a top-down approach to establish hierarchical CPNs in accordance with specified scenarios (i.e., sequence diagrams). This approach makes use of explicitly labeling component states in the sequence diagrams to correlate scenarios. In addition, the techniques of state space analysis and ASK-CTL model checking are used to verify the correctness and consistency of the CPN model with respect to standard and system-specific properties. As the inspiration of the presented approach derives from the development of train control systems, we present an running example of designing the on-board subsystem of a satellite-based train control system to show the feasibility of our approach.