nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

A Formalisation of SysML State Machines in mCRL2

verfasst von : Mark Bouwman, Bas Luttik, Djurre van der Wal

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2, in order to unlock formal verification and model-based testing using the mCRL2 toolset for SysML models. The formalisation focuses on a fragment of SysML used in the railway standardisation project EULYNX. It comprises the semantics of state machines, communication between objects via ports, and an action language called ASAL. It turns out that the generic execution model of SysML state machines can be elegantly specified using the rich data and process languages of mCRL2. This is a big step towards an automated translation as the generic model can be configured with a formal description of a specific set of state machines in a straightforward manner.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Multi-agent Model for Polarization Under Confirmation Bias in Social Networks

Nächstes Kapitel How Adaptive and Reliable is Your Program?

See https://eulynx.eu.

Formal Methods in Railway Signaling Infrastructure Standardization Processes.

https://www.ptc.com/en/products/windchill/integrity/.

Abdelhalim, I., Schneider, S., Treharne, H.: An integrated framework for checking the behaviour of fUML models using CSP. Int. J. Softw. Tools Technol. Transf. 15(4), 375–396 (2013). https://doi.org/10.1007/s10009-012-0243-0CrossRef

Belinfante, A.: JTorX: Exploring Model-Based Testing. Ph.D. thesis, University of Twente, Enschede, Netherlands (2014). http://purl.utwente.nl/publications/91781

Bouwman, M.: mCRL2 model capturing the generic semantics of EULYNX SysML. https://github.com/markuzzz/SysML-to-mCRL2

Bouwman, M., van der Wal, D., Luttik, B., Stoelinga, M., Rensink, A.: What is the point: formal analysis and test generation or a railway standard. In: Baraldi, P., Di Maio, F., Zio, E. (eds.) Proceedings of ESREL2020-PSAM15, pp. 921–928. Research Publishing, Singapore (2020). https://doi.org/10.3850/978-981-14-8593-0_4410-cd

Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Lecture Notes in Computer Science, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2CrossRef

Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press (2014)

Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J.: Towards model checking executable UML specifications in mCRL2. ISSE 6(1–2), 83–90 (2010). https://doi.org/10.1007/s11334-009-0116-1CrossRef

Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J., dos Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. Lecture Notes in Computer Science, vol. 6957, pp. 225–250. Springer, Cham (2010). https://doi.org/10.1007/978-3-642-25271-6_12CrossRef

Kim, S., Carrington, D.A.: A formal model of the UML metamodel: the UML state machine and its integrity constraints. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002: Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol. 2272, pp. 497–516. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_26CrossRef

10.

Kuske, S.: A Formal Semantics of UML State Machines Based on Structured Graph Transformation. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 241–256. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45441-1_19CrossRef

11.

Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Asp. Comput. 11(6), 637–664 (1999). https://doi.org/10.1007/s001659970003CrossRefMATH

12.

Lilius, J., Paltor, I.: vUML: a tool for verifying UML models. In: The 14th IEEE International Conference on Automated Software Engineering, ASE 1999, Cocoa Beach, Florida, USA, 12–15 October 1999, pp. 255–258. IEEE Computer Society (1999). https://doi.org/10.1109/ASE.1999.802301

13.

Lilius, J., Paltor, I.P.: The semantics of UML state machines (1999)

14.

Liu, S., Liu, Y., André, É., Choppy, C., Sun, J., Wadhwa, B., Dong, J.S.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331–346. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38613-8_23CrossRef

15.

Neele, T., Willemse, T.A.C., Groote, J.F.: Solving parameterised boolean equation systems with infinite data through quotienting. In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 216–236. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_11CrossRef

16.

Object Managament Group: OMG Unified Modeling Language, version 2.5.1 (2017). https://www.omg.org/spec/UML/

17.

Object Managament Group: Precise Semantics of UML State Machines (PSSM), version 1.0 (2019). https://www.omg.org/spec/PSSM/

18.

Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: France, R., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46852-8_31CrossRef

19.

Pedroza, G., Apvrille, L., Knorreck, D.: AVATAR: A SysML environment for the formal verification of safety and security properties. In: 11th Annual International Conference on New Technologies of Distributed Systems, NOTERE 2011, Paris, France, 9–13 May 2011, pp. 1–10. IEEE (2011). https://doi.org/10.1109/NOTERE.2011.5957992

20.

Remenska, D., et al.: From UML to process algebra and back: an automated approach to model-checking software design artifacts of concurrent systems. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods. NFM 2013. LNCS, vol. 7871, pp. 244–260. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_17

21.

Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electron. Notes Theor. Comput. Sci. 55(3), 357–369 (2001). https://doi.org/10.1016/S1571-0661(04)00262-2CrossRef

22.

van der Wal, D., Bouwman, M., Stoelinga, M., Rensink, A.: On capturing the EULYNX railway standard with an internal DSL in Java. In: preparation for submission (2021)

23.

Wang, H., Zhong, D., Zhao, T., Ren, F.: Integrating model checking with SysML in complex system safety analysis. IEEE Access 7, 16561–16571 (2019). https://doi.org/10.1109/ACCESS.2019.2892745CrossRef

Titel: A Formalisation of SysML State Machines in mCRL2
verfasst von: Mark Bouwman
Bas Luttik
Djurre van der Wal
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"