Paper Info
Title
Experiences in model driven verification of behavior with UML
Abstract
Model Driven Development (MDD) focuses on the intensive use of models during software development. In this paradigm, models are the central development artifact: transformations are used to derive executable programs, or tests for a given platform. This makes building quality models a cost-effective approach, as the models can be reused for many analysis or generation goals, and not just document a design. However, high quality models are needed for the approach to be successful. Hence the goal of performing analysis of high-level behavioral specifications such as UML, to enhance their quality and detect defects or ensure desired behavior. High-level specifications provide many facilities to handle large specifications (such as hierarchical structuring mechanisms) and provide sophisticated features to handle programming language's rich semantics. However, the price of these features is that these specifications are difficult to analyse, the semantics are not necessarily formally defined, and the complexity of the language features usually limits analysis to manual inspection, or in the best cases simulation. On the other hand, formal specifications have been developed specifically with analysis purposes in mind. In particular, model checking is an automatic approach suitable to analyse formally defined behaviors. However, formal specifications languages such as CSP, PROMELA, Petri nets, etc. have a steep learning curve, and are not cost effective since they are not directly linked to code. In this paper, we explore an approach to integrate formal methods with high-level notations, by translating high-level specifications to formal ones to enable analysis. We are thus bringing Model Driven Engineering to Verification Driven Engineering. We show how this approach was put in practice with UML within the context of the ModelPlex project.
Year
DOI
Venue
2008
10.1007/978-3-642-12566-9_10
Monterey Workshop
Keywords
Field
DocType
model driven development,cost-effective approach,formal method,high-level notation,formal specification,analysis purpose,high-level behavioral specification,high-level specification,formal specifications language,automatic approach,cost effectiveness,petri net,learning curve,model driven engineering,model checking,software development,programming language
Programming language,Petri net,Unified Modeling Language,Model-driven architecture,Computer science,Formal specification,Promela,Formal methods,Software development,Executable
Conference
Volume
ISSN
ISBN
6028
0302-9743
3-642-12565-4
Citations 
PageRank 
References 
4
0.45
22
Authors
2
Name
Order
Citations
PageRank
Fabrice Kordon160361.72
Yann Thierry-Mieg222518.17