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

Abstract

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.

Appendix

A non-hierarchical Colored Petri Net is a nine-tuple $CPN = (P,T,A,{\varSigma },V,C,G,E,I)$, where:

• 1. P is a finite set of places.

• 2. T is a finite set of transitions such that $P\cap T = \emptyset$.

• 3. $A\subseteq P\times T\cup T\times P$ is a set of directed arcs.

• 4. ${\varSigma }$ is a finite set of non-empty color sets.

• 5. V is a finite set of typed variables such that $Type[v]\in {\varSigma }$ for all variables $v\in V$.

• 6. $C:P\rightarrow {\varSigma }$ is a color set function that assigns a color set to each place.

• 7. $G:T\rightarrow EXPR_V$ is a guard function that assigns a guard to each transition t such that $Type[G(t)] = Bool$.

• 8. $E:A\rightarrow EXPR_V$ is an arc expression function that assigns an arc expression to each arc a such that $Type[E(a)] =C(p)_{MS}$ ⁴, where p is the place connected to the arc a.

• 9. $I:P\rightarrow EXPR_\emptyset$ is an initialisation function that assigns an initialisation expression to each place p such that $Type[I(p)] =C(p)_{MS}$.

A hierarchical Colored Petri Net is a four-tuple $CPN_H = (S,SM, PS,FS)$ where:

• 1. S is a finite set of modules. Each module is a Colored Petri Net Module $s =((P^s,T^s,A^s,{\varSigma } ^s,V^s,C^s,G^s,E^s,I^s),T_{sub}^s,P_{port}^s,PT^s)$. It is required that $(P^{s_1}\cup T^{s_1})\cap (P^{s_2}\cup T^{s_2})=\emptyset$ for all $s_1,s_2\in S$ such that $s_1\ne s_2$.

• 2. $SM:T_{sub}\rightarrow S$is a submodule function that assigns a submodule to each substitution transition. It is required that the module hierarchy ⁵ is acyclic.

• 3. PS is a port-socket relation function that assigns a port-socket relation $PS(t)\subseteq P_{sock}(t)\times P_{port}^{SM(t)}$ to each substitution transition t. It is required that $ST(p)=PT(p'),C(p)=C(p')$ and $I(p)\langle \rangle$ for all $(p,p')\in PS(t)$ and all $t\in T_{sub}$.

• 4. $FS\subseteq 2^P$ is set of non-empty fusion sets such that $C(p)=C(p')$ and $I(p)\langle \rangle =I(p')\langle \rangle$ for all $p,p'\in fs$ and all $fs\in FS$.