Paper Info
Title
EMFeR: Model Checking for Object Oriented (EMF) Models
Abstract
For safety critical systems it is desirable to be able to prove system correctness. If your system is based e.g. on statecharts or finite automata you may use model checking techniques as provided e.g. by Spin. If your system uses dynamic object models you may use tools like Alloy or graph based tools like Groove, Henshin, or SDMLib. Unfortunately, most of theses approaches use proprietary languages for the specification of models and model transformations. This has the drawback that in order to verify system properties one has to recode the system and its operations within the specific language of the used verification tool. This is tedious and error prone. After a successful verification within the specific tool, you still do not know whether your actual implementation works correct. To overcome these limitations, this paper outlines our new EMFeR (EMF Engine for Reachability) tool. EMFeR provides complete testing and model checking capabilities for EMF based models. Unlike most other systems, EMFeR uses directly the code of the system under test. You just hand your implementation of the employed model operations to EMFeR as lambda expressions. In addition, you provide some model queries to retrieve model elements to be operated on. Thus, you may implement your system's model operation in plain Java, in Kotlin, in Groovy or whatever and than you may use EMFeR to model check your actual system implementation.
Year
DOI
Venue
2019
10.5220/0007681605110518
MODELSWARD: PROCEEDINGS OF THE 7TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT, 2019
Keywords
Field
DocType
Model Checking,Object Models,EMF
System under test,Programming language,Model checking,Object-oriented programming,Life-critical system,Expression (mathematics),Computer science,Correctness,Finite-state machine,Reachability,Theoretical computer science
Conference
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Christoph Eickhoff100.68
Martin Lange244722.83
Simon-Lennert Raesch300.34
Albert Zündorf444969.12