Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3417990.3419227acmconferencesArticle/Chapter ViewAbstractPublication PagesmodelsConference Proceedingsconference-collections
research-article

Modular deployment of UML models for V&V activities and embedded execution

Published: 26 October 2020 Publication History

Abstract

To design embedded systems, multiple models of their environments are typically required for different purposes such as simulation, verification, and actual execution. Some of these models abstract the actual physical environment to facilitate Verification and Validation (V&V) activities. Others capture the connection to hardware peripherals, necessary to deploy the systems on actual embedded boards. However, mapping a system to different environment models for different purposes remains a complex task for two main reasons. First, the environment is often tightly coupled with the system, and the board used for its execution. Second, formal properties verified during the design phase must be preserved at runtime. To tackle these issues, we propose an approach for designing UML models in a modular way and deploying them for V&V activities or embedded execution. This approach uses UML modularity mechanisms to specify the system in a generic way, and to connect it to a given (abstract or real) environment. This technique has been applied on several UML models of embedded systems to analyze their behaviors by simulation and LTL model-checking before deploying them on embedded STM32 boards.

References

[1]
Jean-Raymond Abrial. 2013. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA.
[2]
Samir Ammour and Philippe Desfray. 2006. A Concern-based Technique for Architecture Modelling Using the UML Package Merge. Electronic Notes in Theoretical Computer Science 163, 1 (2006), 7--18. Proceedings of the First Workshop on Aspect-Based and Model-Based Separation of Concerns in Software Systems (ABMB 2005).
[3]
Gérard Berry. 2007. SCADE: Synchronous Design and Validation of Embedded Control Software. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, S. Ramesh and Prahladavaradan Sampath (Eds.). Springer Netherlands, Dordrecht, 19--33.
[4]
Valentin Besnard, Matthias Brun, Frédéric Jouault, Ciprian Teodorov, and Philippe Dhaussy. 2018. Unified LTL Verification and Embedded Execution of UML Models. In ACM/IEEE 21th International Conference on Model Driven Engineering Languages and Systems (MODELS '18). Copenhagen, Denmark.
[5]
Valentin Besnard, Ciprian Teodorov, Frédéric Jouault, Matthias Brun, and Philippe Dhaussy. 2019. Verifying and Monitoring UML Models with Observer Automata. In ACM/IEEE 22th International Conference on Model Driven Engineering Languages and Systems (MODELS '19). Munich, Germany, 161--171.
[6]
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 (Amsterdam, Netherlands) (SLE 2016). ACM, New York, NY, USA, 84--89.
[7]
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.
[8]
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.
[9]
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 (Gothenburg, Sweden) (ICSE-NIER '18). ACM, New York, NY, USA, 41--44.
[10]
Federico Ciccozzi, Ivano Malavolta, and Bran Selic. 2018. Execution of UML models: a systematic review of research and practice. Software & Systems Modeling (10 April 2018).
[11]
Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. 1989. Compositional Model Checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. 353--362.
[12]
Benoit Combemale and Cédric Brun. 2015. Breathe Life Into Your Designer! http://gemoc.org/breathe-life-into-your-designer.html
[13]
Luca de Alfaro and Thomas A. Henzinger. 2001. Interface Automata. In Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Vienna, Austria) (ESEC/FSE-9). ACM, New York, NY, USA, 109--120.
[14]
Philippe Dhaussy, Jean-Charles Roger, and Frédéric Boniol. 2011. Reducing State Explosion with Context Modeling for Model-Checking. In 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering. 130--137.
[15]
Philippe Dhaussy, Jean-Charles Roger, Luka Leroux, and Frédéric Boniol. 2012. Context Aware Model Exploration with OBP tool to Improve Model-Checking. In ERTS 2012. Toulouse, France, xx.
[16]
N. Hili, J. Dingel, and A. Beaulieu. 2017. Modelling and Code Generation for Real-Time Embedded Systems with UML-RT and Papyrus-RT. In 2017 IEEE/ACM 39th International Conference on Software Engineering Companion (ICSE-C). 509--510.
[17]
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--27.
[18]
Xavier Leroy. 2017. The CompCert C verified compiler: Documentation and user's manual. Intern report. Inria.
[19]
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 (Innsbruck, Austria) (MW '12). ACM, New York, NY, USA, Article 3, 2 pages.
[20]
Geert Monsieur, Monique Snoeck, Raf Haesen, and Wilfried Lemahieu. 2006. PIM to PSM transformations for an event driven architecture in an educational tool. Milestones, Models and Mappings for Model-Driven Architecture (2006), 49.
[21]
OMG. 2017. Unified Modeling Language. https://www.omg.org/spec/UML/2.5.1/PDF
[22]
OMG. 2019. Precise Semantics of UML Composite Structures. https://www.omg.org/spec/PSCS/1.2/PDF
[23]
Richard F. Paige, Dimitrios S. Kolovos, and Fiona A.C. Polack. 2005. Refinement via Consistency Checking in MDA. Electronic Notes in Theoretical Computer Science 137, 2 (2005), 151--161. Proceedings of the REFINE 2005 Workshop (REFINE 2005).
[24]
Sebastien Revol, Géry Delog, Arnaud Cuccurru, and Jérémie Tatibouët. 2018. Papyrus: Moka Overview. https://wiki.eclipse.org/Papyrus/UserGuide/ModelExecution
[25]
Samuel Rouxel, Jean-Philippe Diguet, Guy Gogniat, Nicolas Bulteau, Jonathan Carre-Gourdin, Jean-Etienne Goubard, and Christophe Moy. 2005. UML Framework for PIM and PSM Verification of SDR Systems. In SDR Forum Technical Conference'05. Anaheim, CA, United States.
[26]
Colin Snook and Michael Butler. 2006. UML-B: Formal Modeling and Design Aided by UML. ACM Trans. Softw. Eng. Methodol. 15, 1 (Jan. 2006), 92--122.
[27]
David Steinberg, Frank Budinsky, Marcelo Paternostro, and Ed Merks. 2009. EMF: Eclipse Modeling Framework 2.0 (2nd ed.). Addison-Wesley Professional.
[28]
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 April 2017), 229--245.
[29]
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.
[30]
Oksana Tkachuk, Matthew B. Dwyer, and Corina S. Pasareanu. 2003. Automated Environment Generation for Software Model Checking. In 18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings. 116--127.
[31]
Alanna Zito, Zinovy Diskin, and Juergen Dingel. 2006. Package Merge in UML 2: Practice vs. Theory?. In Model Driven Engineering Languages and Systems, Oscar Nierstrasz, Jon Whittle, David Harel, and Gianna Reggio (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 185--199.

Cited By

View all
  • (2024)A framework for embedded software portability and verification: from formal models to low-level codeSoftware and Systems Modeling10.1007/s10270-023-01144-y23:2(289-315)Online publication date: 1-Feb-2024
  • (2022)A framework for OS portabilityProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3506996(1156-1165)Online publication date: 25-Apr-2022

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings
October 2020
713 pages
ISBN:9781450381352
DOI:10.1145/3417990
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

  • IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 October 2020

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. UML execution
  2. deployment
  3. embedded systems
  4. model-checking
  5. model-driven engineering

Qualifiers

  • Research-article

Funding Sources

  • Davidson Consulting

Conference

MODELS '20
Sponsor:

Acceptance Rates

Overall Acceptance Rate 144 of 506 submissions, 28%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2024)A framework for embedded software portability and verification: from formal models to low-level codeSoftware and Systems Modeling10.1007/s10270-023-01144-y23:2(289-315)Online publication date: 1-Feb-2024
  • (2022)A framework for OS portabilityProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3506996(1156-1165)Online publication date: 25-Apr-2022

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media