|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
IRIT and University of Toulouse (FRANCE)
|
|---|---|
| Method: |
UML
SysML |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
OMEGA2 |
| Domain: |
Embedded Systems.
|
| Period: |
2011
|
| Size: |
n/a
|
| Description: |
Model Driven Engineering (MDE) approaches are being adopted in a large
number of domains. UML and SysML are two examples of languages used in
this context. In the area of embedded software, but not only, one of
the reasons the use of models is interesting is that they allow for
early verification at model level. The early verification is done using
various automation techniques, amongst the most used being model
checking techniques. This work aims at increasing the scalability of
model checking techniques for these modeling languages by proposing a
semantics optimisation approach focused on composite structures, as
defined in UML2 and SysML. The existing semantics was optimized based
on the observation that in most of the cases, the notions of port,
interface, and connector usually present in the hierarchical models of
industrial systems, are much simpler that their complex counterparts
defined by the UML2 standard.
The alternative, optimized semantics yields equivalent representations of the models in terms of labeled transition systems. This qualitative evaluation of the alternative semantics, as implemented in the OMEGA2 framework, was illustrated on the model of an automated teller machine (ATM), by checking that the two LTSs produced by the standard and alternative semantics are strongly bisimilar, using the CADP toolbox. |
| Conclusions: |
Successful applications of formal methods and verification in MDE
require a careful analysis of the correlation between the semantics
of the model and the actual needs of its application domain. General
languages, such as UML, have the huge advantage of being largely known
and applicable. However, they often bring an overhead that proves to be
critical for model-based verification and validation activities.
For the communities using these languages, it may be interesting to
set up a repository of semantic variants, which makes explicit the
details about the induced restrictions, the sufficient conditions for
equivalence with the standard semantics, and the potential gains in
terms of various metrics, including simulation and model checking
capabilities.
|
| Publications: |
[Ober-Ober-Dragomir-Aboussoror-11]
Ileana Ober, Iulian Ober, Iulia Dragomir, and El Abri Aboussoror.
"UML/SysML Semantic Tunings".
Innovations in Systems and Software Engineering 7(4):257-264, 2011.
Available on-line at: http://link.springer.com/article/10.1007/s11334-011-0163-2 |
| Contact: | Ober Ileana IRIT, University Paul Sabatier 118, route de Narbonne F-31062 Toulouse Cedex 9 FRANCE Tel: +33 (0)5 61 55 74 23 Fax: +33 (0)5 61 55 68 47 Email: Ileana.Ober@irit.fr |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page