Wu, D.; Schnieder, E.:
Scenario-Based Modeling of the On-Board of a Satellite-Based Train Control System With Colored Petri Nets.
IEEE Transactions on Intelligent Transportation Systems. Volume: PP (Issue: 99), S. 1 - 17, März 2016.
For the goal of model-based system design and development, this paper exploits the formalism of colored Petri nets (CPNs) to model the on-board subsystem of a satellite-based train control system on the basis of scenarios. The Unified Modeling Language sequence diagrams, which are easily understood by customers, requirement engineers, and software developers, are used 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 to obtain an overall system behavior. A large number of works have investigated scenario synthesis providing approaches or algorithms. These synthesis approaches and algorithms result in either Petri net models that are mainly suitable for scenario validation or other forms of behavior models (e.g., labeled transition systems and statecharts) that may be regarded as design models. Petri nets are well known for describing distributed and concurrent systems. Furthermore, numerous techniques, e.g., simulation, testing, state-space-based techniques, structural methods, and model checking, are currently available for analyzing PN models. Therefore, design models, which integrate all scenarios into a coherent whole suitable for further detailed design, in the form of Petri nets 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 model-based testing are employed to verify the correctness and consistency of the CPN model with respect to standard and system-specific properties. The verification results show that our approach is desirable.