An Approach for the Transformation and Verification of BPMN Models to Colored Petri Nets Models

2020 ◽  
Vol 8 (1) ◽  
pp. 17-49 ◽  
Author(s):  
Said Meghzili ◽  
Allaoua Chaoui ◽  
Martin Strecker ◽  
Elhillali Kerkouche
Keyword(s):  
Petri Nets ◽  
Structural Properties ◽  
Graph Transformation ◽  
Colored Petri Nets ◽  
Model Checker ◽  
Model Driven Engineering ◽  
Model Driven ◽  
Successful Termination ◽  
Cpn Tools

The correctness of transformations has recently begun to attract the attention of the researchers in Model Driven Engineering (MDE). The objective of this article is twofold. First, it presents an approach for transforming BPMN models to Colored Petri nets models using GROOVE and EMF/Xpand tools. Second, it proposes an approach for checking the correctness of the transformation itself. More precisely, we have defined the termination property of the transformation and the preservation of some structural properties of BPMN models by the transformation using the GROOVE graph transformation tool. The authors have also applied the approach on a case study through which the authors have verified the successful termination of the transformation using GROOVE Model Checker and the target model properties using CPN Tools.

Modeling With Colored Petri Nets

2021 ◽  
pp. 397-424
Author(s):  
Dmitry A. Zaitsev ◽  
Tatiana R. Shmeleva
Keyword(s):  
Performance Evaluation ◽  
Petri Nets ◽  
Petri Net ◽  
Real Life ◽  
Colored Petri Nets ◽  
Correctness Proof ◽  
Model Driven ◽  
Cpn Tools ◽  
Complex Models ◽  
And Performance

Aviation and aerospace systems are complex and concurrent and require special tools for their specification, verification, and performance evaluation. The tool in demand should be easily integrated into the standard loop of model-driven development. Colored Petri nets represent a combination of a Petri net graph and a functional programming language ML that makes it powerful and convenient tool for specification of real-life system and solving both tasks: correctness proof i.e. verification and performance evaluation. This chapter studies basic and advanced features of CPN Tools – a powerful modeling system which uses graphical language of colored Petri nets. Starting with a concept of colored hierarhical timed Petri net, it goes through declaration of color sets and functions to peculiarities of hierarchical design of complex models and specification of timed characteristics. The authors accomplish the chapter with a real-life case study of performance evaluation for switched Ethernet network.

scholarly journals A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems

2021 ◽  
Vol 22 (2) ◽  
Author(s):  
Raida Elmansouri ◽  
Said Meghzili ◽  
Allaoua Chaoui
Keyword(s):  
Model Transformation ◽  
Integrated Approach ◽  
Software Systems ◽  
Sequential Process ◽  
Model Checker ◽  
Model Driven Engineering ◽  
Model Driven ◽  
Activity Diagrams ◽  
Uml 2.0

This paper proposes an approach integrating UML 2.0 Activity Diagrams (UML2-AD) and Communicating Sequential Process (CSP) for modeling and verication of software systems. A UML2-AD is used for modeling a software system while CSP is used for verication purposes. The proposed approach consists of another way of transforming UML2-AD models to Communicating Sequential Process (CSP) models. It focuses also on checking the correctness of some properties of the transformation itself. These properties are specified using Linear Temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on Model Driven Engineering (MDE). The meta-modelling is realized using AToMPM tool while the model transformation and the correctness of its properties are realized using GROOVE tool. Finally, we illustrated this approach through a case study.

Modeling With Colored Petri Nets

2019 ◽  
pp. 378-404
Author(s):  
Dmitry A. Zaitsev ◽  
Tatiana R. Shmeleva
Keyword(s):  
Performance Evaluation ◽  
Petri Nets ◽  
Petri Net ◽  
Real Life ◽  
Colored Petri Nets ◽  
Correctness Proof ◽  
Model Driven ◽  
Cpn Tools ◽  
Complex Models ◽  
And Performance

Aviation and aerospace systems are complex and concurrent and require special tools for their specification, verification, and performance evaluation. The tool in demand should be easily integrated into the standard loop of model-driven development. Colored Petri nets represent a combination of a Petri net graph and a functional programming language ML that makes it powerful and convenient tool for specification of real-life system and solving both tasks: correctness proof i.e. verification and performance evaluation. This chapter studies basic and advanced features of CPN Tools – a powerful modeling system which uses graphical language of colored Petri nets. Starting with a concept of colored hierarhical timed Petri net, it goes through declaration of color sets and functions to peculiarities of hierarchical design of complex models and specification of timed characteristics. The authors accomplish the chapter with a real-life case study of performance evaluation for switched Ethernet network.

scholarly journals Mixed-semantics composition of statecharts for the component-based design of reactive systems

2020 ◽  
Vol 19 (6) ◽  
pp. 1483-1517
Author(s):  
Bence Graics ◽  
Vince Molnár ◽  
András Vörös ◽  
István Majzik ◽  
Dániel Varró
Keyword(s):  
Code Generation ◽  
Composite System ◽  
Formal Semantics ◽  
Reactive Systems ◽  
Cyber Physical System ◽  
Test Case ◽  
Model Checker ◽  
Model Driven Engineering ◽  
Design Decisions ◽  
Model Driven

Abstract The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.

Model-driven engineering applied to the development of embedded software for B-mode ultrasound imaging systems - A case study

2014 ◽  
Author(s):  
Haroldo Jose Onisto ◽  
Tiago de Moraes Machado ◽  
Ramon Cravo Fernandes ◽  
Johannes Dantas de Medeiros ◽  
Iliezer Tamagno ◽  
...  
Keyword(s):  
Ultrasound Imaging ◽  
Embedded Software ◽  
Imaging Systems ◽  
Model Driven Engineering ◽  
Model Driven
Sign in / Sign up

Export Citation Format

Share Document