article

A methodology for verifying SysML requirements using activity diagrams

Authors:

Messaoud Rahim,

Malika IoualalenAuthors Info & Claims

Innovations in Systems and Software Engineering, Volume 13, Issue 1

Pages 19 - 33

https://doi.org/10.1007/s11334-016-0281-y

Published: 01 March 2017 Publication History

Abstract

Designing complex and critical systems needs a methodology to ensure the correctness of their specifications. Within an overall approach which considers the validation of SysML designs, this paper proposes a methodology for verifying SysML requirements on activity diagrams. The objective is to define a complete process to formalize and verify SysML functional requirements related to activity diagrams. Our contributions lie, first, in the definition of AcTRL (Activity Temporal Requirement Language), a new language for the formalization of functional requirements at SysML level. Second, in the proposed verification methodology which is guided by the [InlineEquation not available: see fulltext.]verify[InlineEquation not available: see fulltext.] relationships between SysML requirements and activity diagrams. The verification is enabled by formalizing SysML activities with hierarchical coloured Petri nets (HCPNs) and by automatically translating SysML requirements expressed on AcTRL into temporal logic. Our methodology takes into account the hierarchical structure of SysML activities and their relations with SysML requirements to provide a modular and incremental verification. A case study for a ticket vending machine is presented to illustrate the different steps and the benefits of the proposed methodology.

References

[1]

Alavi H, Avrunin G, Corbett J, Dillon L, Dwyer M, Pasareanu C. Specification patterns. http://patterns.projects.cis.ksu.edu. Accessed 22 May 2016

[2]

Autili M, Inverardi P, Pelliccione P (2007) Graphical scenarios for specifying temporal properties: an automated approach. Autom Softw Eng 14(3):293---340

Digital Library

[3]

Berard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2010) Systems and software verification: model-checking techniques and tools, 1st edn. Springer Publishing Company, Incorporated, Berlin

Digital Library

[4]

Cheng A, Christensen S, Mortensen KH (1997) Model checking Coloured Petri Nets-exploiting strongly connected components. DAIMI Report Series 26(519).

[5]

Damm W, Harel D (2001) LSCs: breathing life into message sequence charts. Form Methods Syst Des 19(1):45---80

Digital Library

[6]

Debbabi M, Hassaine F, Jarraya Y, Soeanu A, Alawneh L (2010) Verification and validation in systems engineering: assessing UML/SysML design models, 1st edn. Springer-Verlag New York, Inc, New York

Digital Library

[7]

Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the international conference on software engineering, pp 411---420. IEEE

Digital Library

[8]

Engels G, Soltenborn C, Wehrheim H (2007) Analysis of UML activities using dynamic meta modeling. In: Formal methods for open object-based distributed systems. Springer, Berlin, pp 76---90

Digital Library

[9]

Eshuis R (2006) Symbolic model checking of UML activity diagrams. ACM Trans Softw Eng Methodol 15(1):1---38

Digital Library

[10]

Eshuis R, Wieringa R (2002) Verification support for workflow design with UML activity graphs. In: Proceedings of the 24th international conference on software engineering. ACM, pp 166---176

Digital Library

[11]

Eshuis R, Wieringa R (2004) Tool support for verifying UML activity diagrams. IEEE Trans Softw Eng 30(7):437---447

Digital Library

[12]

Farail P, Goutillet P, Canals A, Le Camus C, Sciamma D, Michel P, Crégut X, Pantel M (2006) The TOPCASED project: a toolkit in open source for critical aeronautic systems design. Ingenieurs de l'Automobile 781:54---59

[13]

Foures D, Albert V, Pascal JC, Nketsa A (2012) Automation of SysML activity diagram simulation with model-driven engineering approach. In: Proceedings of the 2012 symposium on theory of modeling and simulation--DEVS integrative M&S symposium, TMS/DEVS '12. Society for Computer Simulation International, San Diego, pp 11:1---11:6

Digital Library

[14]

Jensen K, Kristensen LM, Wells L (2007) Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transf 9(3):213---254

Digital Library

[15]

Kanso B, Taha S (2013) Temporal constraint support for OCL. In: Software language engineering. Springer, Berlin, pp 83---103

[16]

Knorreck D, Apvrille L, de Saqui-Sannes P (2011) TEPE: a SysML language for time-constrained property modeling and formal verification. ACM SIGSOFT Softw Eng Notes 36(1):1---8

Digital Library

[17]

Linhares MV, de Oliveira RS, Farines J-M, Vernadat F (2007) Introducing the modeling and verification process in SysML. In: Emerging technologies and factory automation (ETFA) IEEE conference. IEEE, pp 344---351

[18]

Michael W, Ekkart K (2003) The Petri net markup language. In: Petri net technology for communication-based systems. Springer, Berlin, pp 124---144

[19]

Nejati S, Sabetzadeh M, Falessi D, Briand L, Coq T (2012) A SysML-based approach to traceability management and design slicing in support of safety certification: framework, tool support, and case studies. Inf Softw Technol 54(6):569---590

Digital Library

[20]

OMG (2010) OMG Systems Modeling Language (OMG SysML$$^{{\rm TM}}$$TM) Version 1.2 Downloadable from http://www.omg.org

[21]

Rahim M, Boukala-Ioualalen M, Hammad A (2014) Petri nets based approach for modular verification of SysML requirements on activity diagrams. In: PNSE'14, a satellite event of Petri Nets 2014 and ACSD 2014, Tunis, Tunisia, pp 233---248

[22]

Rahim M, Hammad A, Ioulalen M (2013) Modular and distributed verification of SysML activity diagrams. In: MODELSWARD 2013, 1st international conference on model-driven engineering and software development, Barcelona, Spain, pp 202---205

[23]

Siamak R (2008) Formal modeling and verification of software models. In: Proceedings of World academy of science, engineering and technology, pp 276---282

[24]

Staines TS (2008) Intuitive mapping of UML 2 activity diagrams into fundamental modeling concept Petri net diagrams and colored Petri nets. In: 15th annual IEEE international conference and workshop on the engineering of computer based systems, 2008. ECBS 2008. IEEE, pp 191---200

Digital Library

[25]

Störrle H (2005) Semantics and verification of data flow in UML 2.0 activities. Electron Notes Theor Comput Sci 127(4):35---52

Digital Library

[26]

Ziemann P, Gogolla M (2003) OCL extended with temporal logic. In: Perspectives of system informatics. Springer, Berlin, pp 351---357

Cited By

Cederbladh JCicchetti ASuryadevara J(2024)Early Validation and Verification of System Behaviour in Model-based Systems Engineering: A Systematic Literature ReviewACM Transactions on Software Engineering and Methodology10.1145/363197633:3(1-67)Online publication date: 15-Mar-2024
https://dl.acm.org/doi/10.1145/3631976
Coudert SApvrille LSultan BHotescu Ode Saqui-Sannes P(2024)Incremental and Formal Verification of SysML ModelsSN Computer Science10.1007/s42979-024-03027-55:6Online publication date: 17-Jul-2024
https://dl.acm.org/doi/10.1007/s42979-024-03027-5
Ding JReniers MLu JWang GFeng LKiritsis DGray JRossi MSprinkle JTolvanen J(2021)Integration of modeling and verification for system model based on KARMA languageProceedings of the 18th ACM SIGPLAN International Workshop on Domain-Specific Modeling10.1145/3486603.3486775(41-50)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1145/3486603.3486775

Index Terms

A methodology for verifying SysML requirements using activity diagrams
1. Software and its engineering
  1. Software creation and management
    1. Software development process management

Index terms have been assigned to the content through auto-classification.

Recommendations

Formal Specification and Probabilistic Verification of SysML Activity Diagrams
TASE '12: Proceedings of the 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering

Model-driven engineering refers to a range of engineering approaches that uses models throughout systems and software development life cycle. Towards sustaining the success in practice of model-driven engineering, we present a probabilistic verification ...
On the Meaning of SysML Activity Diagrams
ECBS '09: Proceedings of the 2009 16th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems

In this paper, we aim to ascribe a meaning to SysML activity diagrams. To this end, we propose a dedicated algebraic-like language, namely activity calculus, and an operational semantics that provides a rigorous and intuitive operational understanding ...
Integrating the SysML and ACME in a Model Driven Engineering Approach to Verify the Web Service Composition
WETICE '15: Proceedings of the 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises

Systems engineering, and especially the modelling of the Web service composition, needs proper means for verification to detect critical issues as soon as possible. The objective of our work is to identify a verifiable subset of SysML (System Modelling ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Innovations in Systems and Software Engineering

Innovations in Systems and Software Engineering Volume 13, Issue 1

March 2017

76 pages

ISSN:1614-5046

Issue’s Table of Contents

Copyright © Copyright © 2017 Springer-Verlag London.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2017

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cederbladh JCicchetti ASuryadevara J(2024)Early Validation and Verification of System Behaviour in Model-based Systems Engineering: A Systematic Literature ReviewACM Transactions on Software Engineering and Methodology10.1145/363197633:3(1-67)Online publication date: 15-Mar-2024
https://dl.acm.org/doi/10.1145/3631976
Coudert SApvrille LSultan BHotescu Ode Saqui-Sannes P(2024)Incremental and Formal Verification of SysML ModelsSN Computer Science10.1007/s42979-024-03027-55:6Online publication date: 17-Jul-2024
https://dl.acm.org/doi/10.1007/s42979-024-03027-5
Ding JReniers MLu JWang GFeng LKiritsis DGray JRossi MSprinkle JTolvanen J(2021)Integration of modeling and verification for system model based on KARMA languageProceedings of the 18th ACM SIGPLAN International Workshop on Domain-Specific Modeling10.1145/3486603.3486775(41-50)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1145/3486603.3486775

View Options

View options

Get Access

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents