Unified LTL Verification and Embedded Execution of UML Models

ABSTRACT

The increasing complexity of embedded systems leads to uncertain behaviors, security flaws, and design mistakes. With model-based engineering, early diagnosis of such issues is made possible by verification tools working on design models. However, three severe drawbacks remain to be fixed. First, transforming design models into executable code creates a semantic gap between models and code. Furthermore, for formal verification, a second transformation (towards a formal language) is generally required, which complicates the diagnosis process. Finally, an equivalence relation between verified formal models and deployed code should be built, proven, and maintained. To tackle these issues, we introduce a UML interpreter that fulfills multiple purposes: simulation, formal verification, and execution on both desktop computer and bare-metal embedded target. Using a single interpreter for all these activities ensures operational semantics consistency. We illustrate our approach on a level crossing example, showing verification of LTL properties on a desktop computer, as well as execution on a stm32 embedded target.

References

1. Joshua Auerbach, David F. Bacon, Bob Blainey, Perry Cheng, Michael Dawson, Mike Fulton, David Grove, Darren Hart, and Mark Stoodley. 2007. Design and Implementation of a Comprehensive Realtime Java Virtual Machine. In Proceedings of the 7th ACM & IEEE International Conference on Embedded Software (EMSOFT '07). ACM, New York, NY, USA, 249--258.
2. Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. 2012. LTL to Büchi Automata Translation: Fast and More Deterministic. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara König (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 95--109.
3. Mojtaba Bagherzadeh, Nicolas Hili, and Juergen Dingel. 2017. Model-level, Platform-independent Debugging in the Context of the Model-driven Development of Realtime Systems. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017). ACM, New York, NY, USA, 419--430.
4. Jason Baker, Antonio Cunei, Chapman Flack, Filip Pizlo, Marek Prochazka, Jan Vitek, Austin Armbruster, Edward Pla, and David Holmes. 2006. A Realtime Java Virtual Machine for Avionics - An Experience Report. In Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS '06). IEEE Computer Society, Washington, DC, USA, 384--396.
5. Valentin Besnard, Matthias Brun, Philippe Dhaussy, Frédéric Jouault, David Olivier, and Ciprian Teodorov. 2017. Towards one Model Interpreter for Both Design and Deployment. In 3rd International Workshop on Executable Modeling (EXE 2017). Austin, United States.
6. Erwan Bousse, Jonathan Corley, Benoit Combemale, Jeff Gray, and Benoit Baudry. 2015. Supporting Efficient and Advanced Omniscient Debugging for xDSMLs. In Proceedings of the 2015 ACM SIGPLAN International Conference on Software Language Engineering (SLE 2015). ACM, New York, NY, USA, 137--148.
7. Erwan Bousse, Thomas Degueule, Didier Vojtisek, Tanja Mayerhofer, Julien Deantoni, and Benoit Combemale. 2016. Execution Framework of the GEMOC Studio (Tool Demo). In Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering (SLE 2016). ACM, New York, NY, USA, 84--89.
8. A. Caracas, T. Kramp, M. Baentsch, M. Oestreicher, T. Eirich, and I. Romanov. 2009. Mote Runner: A Multi-language Virtual Machine for Small Embedded Devices. In Proceedings of the 2009 Third International Conference on Sensor Technologies and Applications (SENSORCOMM '09). IEEE Computer Society, Washington, DC, USA, 117--125.
9. Asma Charfi Smaoui, Chokri Mraidha, and Pierre Boulet. 2012. An Optimized Compilation of UML State Machines. In ISORC - 15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing. Shenzhen, China.
10. Federico Ciccozzi. 2014. From Models to Code and Back: A Round-trip Approach for Model-driven Engineering of Embedded Systems. Ph.D. Dissertation. Mälardalen University, Embedded Systems.
11. Federico Ciccozzi. 2018. Unicomp: A Semantics-aware Model Compiler for Optimised Predictable Software. In Proceedings of the 40th International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER '18). ACM, New York, NY, USA, 41--44.
12. Federico Ciccozzi, Ivano Malavolta, and Bran Selic. 2018. Execution of UML models: a systematic review of research and practice. Software & Systems Modeling (10 Apr 2018).
13. Julien Deantoni, Papa Issa Diallo, Joël Champeau, Benoit Combemale, and Ciprian Teodorov. 2014. Operational Semantics of the Model of Concurrency and Communication Language. Research Report RR-8584. INRIA. 23 pages.
14. Andreas Gaiser and Stefan Schwoon. 2009. Comparison of Algorithms for Checking Emptiness on Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (OpenAccess Series in Informatics (OASIcs)), Petr Hlinený, Václav Matyáš, and Tomáš Vojnar (Eds.), Vol. 13. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 18--26.
15. Eran Gery, David Harel, and Eldad Palachi. 2002. Rhapsody: A Complete Life-Cycle Model-Based Development System. In Integrated Formal Methods, Michael Butler, Luigia Petre, and Kaisa Sere (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--10.
16. Ian Wilkie, Adrian King, Mike Clarke, Chas Weaver, Chris Raistrick, and Paul Francis. 2003. UML ASL Reference Guide. http://www.ooatool.com/docs/ASL03.pdf Kennedy Carter.
17. Galois Inc. {n. d.}. The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen. https://github.com/GaloisInc/HaLVM
18. Project Technology Inc. 2008. Object Action Language Reference Manual. http://www.ooatool.com/docs/OAL08.pdf
19. Padma Iyenghar, Elke Pulvermueller, Clemens Westerkamp, Juergen Wuebbelmann, and Michael Uelschen. 2017. Model-Based Debugging of Embedded Software Systems. Springer New York, New York, NY, 107--132.
20. Frédéric Jouault, Ciprian Teodorov, Jérôme Delatour, Luka Le Roux, and Philippe Dhaussy. 2014. Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD. Génie logiciel 109 (June 2014).
21. Agnes Lanusse, Yann Tanguy, Huascar Espinoza, Chokri Mraidha, Sebastien Gerard, Patrick Tessier, Remi Schnekenburger, Hubert Dubois, and François Terrier. 2009. Papyrus UML: an open source toolset for MDA. In Proceedings of the Fifth European Conference on Model-Driven Architecture Foundations and Applications (ECMDAFA 2009). 1--4.
22. Daniel Leroux, Martin Nally, and Kenneth Hussey. 2006. Rational Software Architect: A tool for domain-specific modeling. IBM systems journal 45, 3 (2006), 555--568.
23. Philip Levis and David Culler. 2002. Maté: A Tiny Virtual Machine for Sensor Networks. SIGPLAN Not. 37, 10 (Oct. 2002), 85--95.
24. Tanja Mayerhofer and Philip Langer. 2012. Moliz: A Model Execution Framework for UML Models. In Proceedings of the 2nd International Master Class on Model-Driven Engineering: Modeling Wizards (MW '12). ACM, New York, NY, USA, Article 3, 2 pages.
25. Tanja Mayerhofer, Philip Langer, Manuel Wimmer, and Gerti Kappel. 2013. xMOF: Executable DSMLs Based on fUML. In Software Language Engineering, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.). Springer International Publishing, Cham, 56--75.
26. M Mohlin. 2011. Using the UML Action Language in Rational Software Architect.
27. OMG. 2017. Action Language for Foundational UML (Alf). www.omg.org/spec/ALF/1.1/PDF
28. OMG. 2017. Semantics of a Foundational Subset for Executable UML Models. https://www.omg.org/spec/FUML/1.3/PDF
29. OMG. 2017. Unified Modeling Language. https://www.omg.org/spec/UML/2.5.1/PDF
30. Gergely Pintér and István Majzik. 2003. Automatic Code Generation Based on Formally Analyzed UML Statechart Models. In Formal Methods for Railway Operation and Control Systems (Proceedings of the FORMS-2003 Conference), G. Tarnai and E. Schnieder (Eds.). L'Harmattan, Budapest, Hungary, 45--52.
31. Gergely Pintér and István Majzik. 2003. Program Code Generation based on UML Statechart Models. Periodica Polytechnica 47, 3-4 (2003), 187--204.
32. Becky Plummer, Mukul Khajanchi, and Stephen A. Edwards. 2006. An Esterel Virtual Machine for Embedded Systems. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP), International Workshop on Synchronous Languages, Applications, and Programming (SLAP'06) (Ed.), Vol. 126. Vienna, Austria, 912--917.
33. Sebastien Revol, Géry Delog, Arnaud Cuccurru, and Jérémie Tatibouët. 2018. Papyrus: Moka Overview. https://wiki.eclipse.org/Papyrus/UserGuide/ModelExecution
34. Tim Schattkowsky and Wolfgang Muller. 2005. Transformation of UML State Machines for Direct Execution. In Proceedings of the 2005 IEEE Symposium on Visual Languages and Human-Centric Computing (VLHCC '05). IEEE Computer Society, Washington, DC, USA, 117--124.
35. Doug Simon and Cristina Cifuentes. 2005. The Squawk Virtual Machine: Java™on the Bare Metal. In Companion to the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA '05). ACM, New York, NY, USA, 150--151.
36. Ciprian Teodorov, Philippe Dhaussy, and Luka Le Roux. 2017. Environment-driven reachability for timed systems. International Journal on Software Tools for Technology Transfer 19, 2 (01 Apr 2017), 229--245.
37. Ciprian Teodorov, Luka Le Roux, Zoé Drey, and Philippe Dhaussy. 2016. Past-Free{ze} Reachability Analysis: Reaching further with DAG-directed exhaustive state-space analysis. Software Testing, Verification and Reliability 26, 7 (2016), 516--542.
38. Matias Ezequiel Vara Larsen, Julien Deantoni, Benoit Combemale, and Frédéric Mallet. 2015. A Behavioral Coordination Operator Language (BCOoL). In International Conference on Model Driven Engineering Languages and Systems (MODELS), Timothy Lethbridge, Jordi Cabot, and Alexander Egyed (Eds.). ACM, Ottawa, Canada, 462.
39. Markus Voelter, Daniel Ratiu, Bernhard Schaetz, and Bernd Kolb. 2012. Mbeddr: An Extensible C-based Programming Language and IDE for Embedded Systems. In Proceedings of the 3rd Annual Conference on Systems, Programming, and Applications: Software for Humanity (SPLASH 12). ACM, New York, NY, USA, 121--140.

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

    • Embedded systems

      • Embedded software

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification