Software & Systems Modeling

, Volume 17, Issue 1, pp 295–317 | Cite as

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

Regular Paper

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.

Keywords

Scenario System design Modeling Verification Colored Petri nets Train control system 

References

  1. 1.
    Aarhus University: CPN Tools Homepage. http://cpntools.org/ (2000)
  2. 2.
    Ameedeen, M.A., Bordbar, B.: A model driven approach to represent sequence diagrams as free choice Petri nets. In: 2008 12th International IEEE Enterprise Distributed Object Computing Conference (EDOC), pp. 213–221Google Scholar
  3. 3.
    Amyot, D., Eberlein, A.: An evaluation of scenario notations and construction approaches for telecommunication systems development. Telecommun. Syst. 24(1), 61–94 (2003)CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATHGoogle Scholar
  5. 5.
    Barbu, G.: SADT for elaboration and assessment of functional specifications of GNSS supported operation on low traffic density lines. In: Proceedings of Symposium FORMS/FORMAT 2008. L’Harmattan, Budapest and Hungary (2008)Google Scholar
  6. 6.
    Bjørner, D.: On the use of formal methods in software development. In: Proceedings of the 9th International Conference on Software Engineering, pp. 17–29 (1987)Google Scholar
  7. 7.
    Bjørner, D., George, C.W., Hansen, B.S., Laustrup, H., Prehn, S.: A Railway system—coordination ’97: Case Study Workshop Example. UNU/IIST Report No. 93 (1996)Google Scholar
  8. 8.
    CENELEC: EN 50126–1:1999. Railway applications—the specification and demonstration of reliability, availability, maintainability and safety (RAMS)—Part 1: basic requirements and generic process (1999)Google Scholar
  9. 9.
    CENELEC: EN 50128:2001. Railway applications—communications, signalling and processing systems—software for railway control and protection systems (2001)Google Scholar
  10. 10.
    Chen, L., Tang, T., Zhao, X., SchniedeR, E.: Verification of the safety communication protocol in train control system using colored Petri net. Reliab. Eng. Syst. Saf. 100, 8–18 (2012)CrossRefGoogle Scholar
  11. 11.
    Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured Petri nets exploiting strongly connected components. DAIMI report series 26(519) (1997)Google Scholar
  12. 12.
    Chiappini, A., Cimatti, A., Porzia, C., Rotondo, G., Sebastiani, R., Traverso, P., Villafiorita, A.: Formal Specification and Development of a Safety-Critical Train Management System. Computer Safety, Reliability and Security. Springer, NewYork (1999)Google Scholar
  13. 13.
    Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Form. Asp. Comput. 10(4), 361–380 (1998)CrossRefMATHGoogle Scholar
  14. 14.
    Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)CrossRefGoogle Scholar
  15. 15.
    Damas, C., Lambeau, B., van Lamsweerde, A.: Scenarios, goals, and state machines: a win-win partnership for model synthesis. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 197–207 (2000)Google Scholar
  16. 16.
    Drewes, J., May, J., SchniedeR, E., König, N.: Structured approach of a generic (signalling) hazard list for railway (interlocking) systems. In: Proceedings of the 5th European Congress and Exhibition on Intelligent Transport Systems and Services. Hannover and Germany (2005)Google Scholar
  17. 17.
    Elkoutbi, M., Keller, R.K.: User interface prototyping based on UML scenarios and high-level Petri nets. Application Theory Petri Nets, pp. 166–186. Springer, Berlin, Heidelberg (2000)Google Scholar
  18. 18.
    Esparza, J., Schröter, C.: Unfolding based algorithms for the reachability problem. Fundam. Inform. 47(3–4), 231–245 (2001)MathSciNetMATHGoogle Scholar
  19. 19.
    Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M., Westergaard, M.: Towards automatic code generation from process-partitioned coloured Petri nets. In: Proceedings of 10th CPN Workshop, pp. 41–60Google Scholar
  20. 20.
    Fukuda, M., Hirao, Y., Ogino, T.: VDM specification of an interlocking system and a simulator for its validation. In: Proceedings of 9th IFAC Symposium on Control in Transportation Systems 2000, pp. 187–192. Braunschweig and Germany (2000)Google Scholar
  21. 21.
    Girault, C., Valk, R.: Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Springer, NewYork (2001)MATHGoogle Scholar
  22. 22.
    Hansen, K.M.: Validation of a railway interlocking model. In: FME’94: Industrial Benefit of Formal Methods, vol. 873, pp. 582–601 (1994)Google Scholar
  23. 23.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)MathSciNetCrossRefMATHGoogle Scholar
  24. 24.
    Harper, R.: Programming in Standard ML. http://www.cs.cmu.edu/rwh/smlbook/book.pdf (2011)
  25. 25.
    Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)CrossRefGoogle Scholar
  26. 26.
    Meyer zu Hörste, M.: Modelling and simulation of train control systems using Petri nets. In: FMRail Workshop, vol. 3. St. Pölten and Österreich (1999)Google Scholar
  27. 27.
    Meyer zu Hörste, M., SchniedeR, E.: Modelling functionality of train control systems using Petri nets. In: FM-RAIL-BOK Workshop. Madrid (2013)Google Scholar
  28. 28.
    Meyer zu Hörste, M., Weber, I., Illgen, I., Schrom, H., SchniedeR, E.: Distributed multi-train simulation with simulators for real components. In: Proceedings of Computers in Railways VII 2000-COMPRAIL 2000, pp. 1291–1300. WIT Press, Bologna and Italy (2000)Google Scholar
  29. 29.
    ITU-T: Message Sequence Chart (MSC): ITU-T Rec. Z.120 (02/2011) (2011)Google Scholar
  30. 30.
    Janhsen, A., Lemmer, K., Ptok, B., SchniedeR, E.: Formal specifications of the european train control system. In: Proceedings of 8th IFAC Symposium on Transportation Systems, pp. 1215–1220. China (1997)Google Scholar
  31. 31.
    Janota, A., Zahradník, J.: UML—an object oriented approach to formal specification of safety relevant systems. In: 4th International Scientific Conference ELEKTRO 2001. Žilina and Slovak Republic (2001)Google Scholar
  32. 32.
    Jansen, L., Meyer zu Hörste, M., Schniede R.E.: Technical issues in modelling the European train control system (ETCS) using coloured petri nets and the Design/CPN tools. In: Proceedings of the Workshop on Practical Use of Coloured Petri Nets and Design/CPN, pp. 103–115. Aarhus and Denmark (1998)Google Scholar
  33. 33.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, NewYork (2009)CrossRefMATHGoogle Scholar
  34. 34.
    Jones, C.B.: Systematic software development using VDM, vol. 2, 2nd edn. Prentice Hall Englewood Cliffs, NJ (1986)Google Scholar
  35. 35.
    Katsaros, P.: A roadmap to electronic payment transaction guarantees and a colored Petri net model checking approach. Inf. Softw. Technol. 51(2), 235–257 (2009)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. Ph.D. thesis, University of Newcastle upon Tyne, UK (2003)Google Scholar
  37. 37.
    McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 45–65 (1995)CrossRefMATHGoogle Scholar
  38. 38.
    Krüger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to statecharts. Distributed and Parallel Embedded Systems, pp. 61–71. Springer (1999)Google Scholar
  39. 39.
    Lautenbach, K.: Reproducibility of the empty marking. Appl. Theory Petri Nets 2002, 281–300 (2002)MathSciNetMATHGoogle Scholar
  40. 40.
    Lecomte, T., Servat, T., Pouzaucre, G.: Formal methods in safety-critical railway systems. In: Proc. Brazilian Symposium on Formal Methods: SMBF (2007)Google Scholar
  41. 41.
    Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Signal+Draht 3, 57–63 (2009)Google Scholar
  42. 42.
    Mortensen, K.H.: Automatic code generation from coloured Petri nets for an access control system. In: Second Workshop on Practical Use of Coloured Petri Nets and Design/CPN, Aarhus, Denmark, pp. 41–58. Citeseer (1999)Google Scholar
  43. 43.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  44. 44.
    Nielsen, M., Havelund, K., Wagner, K.R., George, C.: The RAISE language, method and tools. Form. Asp. Comput. 1(1), 85–114 (1989)CrossRefGoogle Scholar
  45. 45.
    Object Management Group: Unified Modeling Language. http://www.uml.org/ (2013)
  46. 46.
    Object Management Group: Object Constraint Language: Version 2.4. http://www.omg.org/spec/OCL/2.4/PDF/ (2014)
  47. 47.
    Object Management Group: OMG Unified Modeling Language (OMG UML), Superstructure: Version 2.2. http://www.omg.org/spec/UML/2.2/Superstructure (2009)
  48. 48.
    Padberg, J., Jansen, L., SchniedeR, E., Ehrig, H., Heckel, R.: Cooperability in train control systems: specification of scenarios using open nets. J. Integr. Des. Process Sci. 5(1), 3–21 (2001)Google Scholar
  49. 49.
    Philippi, S.: Automatic code generation from high-level Petri-nets for model driven systems engineering. J. Syst. Softw. 79(10), 1444–1455 (2006)CrossRefGoogle Scholar
  50. 50.
    Pope, M., Drewes, J., May, J.: Generic hazard list for railway systems. In: 7th World Congress on Railway Research—WCRR 2006. Montréal and Canada (2006)Google Scholar
  51. 51.
    Rástočný, K., Janota, A., Zahradník, J.: The use of UML for development of a railway interlocking system. In: Integration of Software Specification Techniques for Applications in Engineering, Lecture Notes in Computer Science, vol. 3147, pp. 174–198. Springer (2004)Google Scholar
  52. 52.
    Ross, D.T.: Structured analysis (SA): a language for communicating ideas. IEEE Trans. Softw. Eng. (1), 16–34 (1977)Google Scholar
  53. 53.
    Stadlmann, B.: Systematic UML-design used in the development of a basic train control system for regional branch lines. In: FORMS/FORMAT 2004, pp. 71–78. Beyrich DigitalService, Germany (2004)Google Scholar
  54. 54.
    Stadlmann, B., Kaiser, F., Maihofer, S.: Rechnergestütztes Zugleitsystem für die Pinzgauer Lokalbahn. Signal+Draht 5, 28–33 (2012)Google Scholar
  55. 55.
    Tretmans, J.: Model Based Testing with Labelled Transition Systems, Lecture Notes in Computer Science, vol. 4949. Springer, Berlin (2008)Google Scholar
  56. 56.
    Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)CrossRefGoogle Scholar
  57. 57.
    Whittle, J., Jayaraman, P.K.: Synthesizing hierarchical state machines from expressive scenario descriptions. ACM Trans. Softw. Eng. Methodol. 19(3), 1–45 (2010)CrossRefGoogle Scholar
  58. 58.
    Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: Proceedings of the 2000 International Conference on Software Engineering, pp. 314–323 (2000)Google Scholar
  59. 59.
    Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference. Vol. 16, pp. 309–316 (2003)Google Scholar
  60. 60.
    Wu, D.: Verifiable Design of a Satellite-based Train Control System with Petri Nets. Ph.D. thesis, Technische Universität Braunschweig, Braunschweig and Germany (2014)Google Scholar
  61. 61.
    Wu, D., SchniedeR, E., Lu, D., Manz, H.: Realistic modelling of train control system with coloured Petri nets. In: Proceedings of 13th IFAC Symposium on Control in Transportation Systems (CTS 2012), vol. 13, pp. 19–23. Sofia and Bulgaria (2012)Google Scholar
  62. 62.
    Zurawski, R., Zhou, M.: Petri nets and industrial applications: a tutorial. IEEE Trans. Ind. Electron. 41(6), 567–583 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2016

Authors and Affiliations

  1. 1.National Research Center of Railway Safety AssessmentBeijing Jiaotong UniversityBeijingChina
  2. 2.Institute for Traffic Safety and Automation EngineeringTechnische Universität BraunschweigBraunschweigGermany

Personalised recommendations