research-article

Time properties dedicated transformation from UML-MARTE activity to time transition system

Authors:

Ning Ge,

Marc Pantel,

Xavier CrégutAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 37, Issue 4

Pages 1 - 8

https://doi.org/10.1145/2237796.2237807

Published: 16 July 2012 Publication History

Get Access

Abstract

Critical Real-Time Systems (RTS) have strong requirements concerning system's reliability. UML and its profile MARTE are standardized modeling languages widely accepted by industrial designers to cope with the development of complex RTS. Relying on Model-Driven Engineering (MDE), time properties verification of UML-MARTE specifications at early phases of the system lifecycle becomes possible. A key issue is to eliminate the gap between UML semi-formal semantics and fully formal executable semantics using model transformation. The model transformation must guarantee the consistency between high-level user models and lowerlevel verification models. Meanwhile, it should guarantee that the subsequent verification is not too expensive and can be applied to real size industrial models. This paper presents an approach to translate UML-MARTE Activity Diagrams into Time Transition System (TTS) with the aim of efficiently verifying time properties in RTS. TTS is a generalization of Time Petri Nets (TPN) with the priority and data handling at the transition level, supported by TINA model checker. This contribution focuses on how to define the TTS formal semantics to avoid the core problem of state space explosion in model checking. This work has been integrated in a time properties verification framework for UML-MARTE RTS specifications. The proposed method is evaluated using a representative case study. Experimental results are given to demonstrate the method's performance.

References

[1]

E. Andrade, P. Maciel, G. Callou, and B. Nogueira. A methodology for mapping sysml activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints. In Digital Society, 2009. ICDS '09., 2009.

Digital Library

Google Scholar

[2]

Sabine Boufenara, Kamel Barkaoui, Faiza Belala, and Hanifa Boucheneb. Mapping uml activity diagrams to analyzable petri net models. In Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011), September 2011.

Google Scholar

[3]

B. Berthomieu, P.-O. Ribet, and F. Vernadat. The tool tina - construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research, 42(14):2741--2756, 2004.

Crossref

Google Scholar

[4]

Ning Ge and Marc Pantel. Time properties verification framework for uml-marte safety critical real-time systems. In 8th European Conference on Modelling Foundations and Applications (ECMFA'2012), July 2012.

Digital Library

Google Scholar

[5]

Juan Pablo López-Grao, José Merseguer, and Javier Campos. From uml activity diagrams to stochastic petri nets: application to software performance engineering. In 4th international workshop on Software and performance, WOSP '04, pages 25--36, New York, NY, USA, 2004. ACM.

Digital Library

Google Scholar

[6]

P. Merlin and D. Farber. Recoverability of communication protocols-implications of a theoretical study. Communications, IEEE Transactions on, 24(9):1036--1043, sep 1976.

Crossref

Google Scholar

[7]

Object Management Group, Inc. OMG Unified Modeling LanguageTM (OMG UML), Superstructure, February 2009.

Google Scholar

[8]

Object Management Group, Inc. UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems Version 1.0, November 2009.

Google Scholar

[9]

Yann Thierry-Mieg and Lom-Messan Hillah. Uml behavioral consistency checking using instantiable petri nets. Innovations in Systems and Software Engineering, 4(3):293--300, 2008.

Crossref

Google Scholar

[10]

Nianhua Yang, Huiqun Yu, Hua Sun, and Zhilin Qian. Mapping uml activity diagrams to analyzable petri net models. In 10th International Conference on Quality Software (QSIC'2010), pages 369-372, july 2010.

Digital Library

Google Scholar

Cited By

View all

Ge NDieumegard AJenn EdaAusbourg BAit-Ameur Y(2017)Formal development process of safety-critical embedded human machine interface systems2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2017.8285636(1-8)Online publication date: Sep-2017
https://doi.org/10.1109/TASE.2017.8285636
Ge NPantel MZilio S(2017)Formal verification of user-level real-time property patterns2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2017.8285630(1-8)Online publication date: Sep-2017
https://doi.org/10.1109/TASE.2017.8285630
Ge NPantel M(2012)Time properties verification framework for UML-MARTE safety critical real-time systemsProceedings of the 8th European conference on Modelling Foundations and Applications10.1007/978-3-642-31491-9_27(352-367)Online publication date: 2-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31491-9_27

Recommendations

Model Checking UML Activity Diagrams in FDR
ICIS '09: Proceedings of the 2009 Eigth IEEE/ACIS International Conference on Computer and Information Science

The Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML Activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, ...
Transformation process of RTS scheduling analysis requirements from UML/MARTE to dynamic priority time Petri Nets

The real-time system (RTS) design is a major challenge due to the complexity of the considered application and the appearance of multiprocessor architectures. Most of the research in this area is interested in high abstraction level methods to decrease ...
Timing consistency checking for UML/MARTE behavioral models

UML/MARTE model-driven development approaches are gaining attention in developing real-time embedded software (RTES). UML behavioral models with MARTE annotations are used to describe timing behaviors and timing characteristics of RTES. Particularly, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 37, Issue 4

July 2012

182 pages

ISSN:0163-5948

DOI:10.1145/2237796

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 July 2012

Published in SIGSOFT Volume 37, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
174
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ge NDieumegard AJenn EdaAusbourg BAit-Ameur Y(2017)Formal development process of safety-critical embedded human machine interface systems2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2017.8285636(1-8)Online publication date: Sep-2017
https://doi.org/10.1109/TASE.2017.8285636
Ge NPantel MZilio S(2017)Formal verification of user-level real-time property patterns2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2017.8285630(1-8)Online publication date: Sep-2017
https://doi.org/10.1109/TASE.2017.8285630
Ge NPantel M(2012)Time properties verification framework for UML-MARTE safety critical real-time systemsProceedings of the 8th European conference on Modelling Foundations and Applications10.1007/978-3-642-31491-9_27(352-367)Online publication date: 2-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31491-9_27

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Model Checking UML Activity Diagrams in FDR

Transformation process of RTS scheduling analysis requirements from UML/MARTE to dynamic priority time Petri Nets

Timing consistency checking for UML/MARTE behavioral models