Cross modeling of embedded systems using SysML and Petri Nets

• Autorzy: Szmuc Wojciech , Szmuc Tomasz
• Języki publikacji: EN

Abstrakty

EN

Cross modeling in embedded systems development is proposed in the paper. The main idea consists in a translation of SysML artifacts into the related Coloured Petri Net (CPN) models, which may be verified directly or using other tools, e.g. Temporal Logic Provers. The paper is an extension of [20] mainly by insertion of sequence diagrams (SysML) and presentation of their mapping into CPN models. The additional part describes communication features and completes the cross modeling approach.

Słowa kluczowe

EN

embedded system; cross modeling; formal verification

PL

systemy wbudowane; modelowanie krzyżowe; formalna weryfikacja

• Wydawca: Lodz University of Technology. Department of Microelectronics and Computer Science
• Czasopismo: International Journal of Microelectronics and Computer Science
• Rocznik: 2018
• Tom: Vol. 9, nr 2
• Strony: 60--65
• Opis fizyczny: Bibliogr. 21 poz.

Twórcy

autor

Szmuc Wojciech

• Department of Applied Computer Science, AGH University of Science and Technology, Kraków, Poland

autor

Szmuc Tomasz

• Department of Applied Computer Science, AGH University of Science and Technology, Kraków, Poland

Bibliografia

• [1] J.-P. Blanquart, J.-M. Astruc, P. Baufreton, J.-L. Boulanger, H. Delseny, J. Gassino, et al., “Criticality categories across safety standards in different domains “, ERTS2 Congress. Embedded Real Time Software and Systems, 2012, pp. 3–4.
• [2] J. Boercsoek, JM. Schwarz, E. Ugljesa, P. Holub, and A. Hayek, “High-availability controller concept for steering systems: The degradable safety controller”, Recent Researches in Circuits, Systems, Communications and Computers, WSEAS. 2011, pp. 222–228.
• [3] B. Cook, H. Khaaaf, and N. Piterman “Verifying increasingly expressive Temporal Logics for infinite-state systems”, Journal of the ACM, vol. 64, No 2, May 2017, Article 15.
• [4] CPN web: http://cpntools.org/
• [5] L. Delligatti, SysML Distilled. A Brief Guide to the Systems Modelling Language, Addison-Wesley, 2014.
• [6] DO-178C, Software Considerations in Airborne Systems and Equipment Certification
• [7] P.H. Feiler, and D.P. Gluch, Model-Based Engineering using AADL. An Introduction to the SAE Architecture Analysis & Design Language”, Addison-Wesley, 2012.
• [8] S. Friedental, A. Moore, and R. Steiner, “A Practical Guide to SysML. The System Modeling Language”, Morgan Kaufman OMG Press, 2010.
• [9] R. Gore, J. Thomson, and F. Widmann, “An experimental comparison of theorem provers for CT, Proceedings of the 2011 International Symposium on Temporal Representation and Reasoning, IEEE Computer Society, 2011, pp. 49-56.
• [10] K. Greb, A. Seely, Design of Microcontrollers for Safety Critical Operation (ISO 26262 Key Differences from IEC 61508), 2009.
• [11] IEC 61508 Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related Systems (E/E/PE, or E/E/PES).
• [12] Road vehicles – Functional safety, ISO 26262.
• [13] K. Jensen, and L. M. Kristensen, Coloured Petri Nets. Modelling and Valiation of Concurrent Systems, Springer, 2009.
• [14] NuSMV, a new symbolic model checker: http://nusmv.fbk.eu/
• [15] Papirus, https://www.isis-papyrus.com/software
• [16] D. Rosenberg, and S. Mancarella: “Embedded systems development using SysML”, Sparx Systems Pty Ltd and ICONIX, 2010
• [17] S. Samolej, and T. Szmuc, “Time constrains modeling and verification using Timed Coloured Petri Nets, Proceedings of the 28th IFAC/IFIP Workshop on the Real Time Programming, Elsevier Science Ltd, 2005, pp. 127-132.
• [18] W. Szmuc, Modelling of Selected UML 2.0 Diagrams with Coloured Petri Nets. PhD Report, Supervisor M. Szpyrka, AGH 2014
• [19] W. Szmuc, and T. Szmuc, “Modeling UML object event handling with Petri Nets. Towards improvement of embedded systems analysis and design”, 23rd International Conference on “Mixed Design and Integrated Circuits and Systems, MIXDES 2016, June 2-25, 2016, Łódź, Poland,pp. 454-457.
• [20] W. Szmuc, and T. Szmuc, ”Towards Embedded Systems Formal Verification. Translation from SysML into Petri Nets”, Proceedings of the 25th International Conference “Mixed Design of Integrated Circuits and Systems”, MIXDES 2018, June 21-23, 2018, Gdynia, Poland, pp.422-425.
• [21] Verics model checker: http://verics.ipipan.waw.pl/

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).