Abstract
| Original language | English |
|---|---|
| Title of host publication | Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS) |
| Subtitle of host publication | Uppsala, Sweden, 29th April 2017 |
| Editors | Holger Hermanns, Peter Höffner |
| Publisher | arXiv.org |
| Pages | 217-229 |
| DOIs | |
| Publication status | Published - Apr 2017 |
| Event | 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017 - Uppsala, Sweden Duration: 29 Apr 2017 → 29 Apr 2017 Conference number: 2 http://mars-workshop.org/mars2017/ |
Publication series
| Name | EPTCS - Electronic Publications in Theoretical Computer Science |
|---|---|
| Volume | 244 |
| ISSN (Print) | 2075-2180 |
Conference
| Conference | 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017 |
|---|---|
| Abbreviated title | MARS |
| Country | Sweden |
| City | Uppsala |
| Period | 29/04/17 → 29/04/17 |
| Internet address |
Fingerprint
Keywords
- Model Driven Engineering
- Metamodelling
- Model Transformaton
- Java bytecode
- UPPAAL
Cite this
}
A Model-Derivation Framework for Software Analysis. / Yildiz, Bugra M.; Rensink, Arend ; Bockisch, Christoph; Aksit, Mehmet .
Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS): Uppsala, Sweden, 29th April 2017. ed. / Holger Hermanns; Peter Höffner. arXiv.org, 2017. p. 217-229 (EPTCS - Electronic Publications in Theoretical Computer Science; Vol. 244).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - A Model-Derivation Framework for Software Analysis
AU - Yildiz, Bugra M.
AU - Rensink, Arend
AU - Bockisch, Christoph
AU - Aksit, Mehmet
PY - 2017/4
Y1 - 2017/4
N2 - Model-based verification allows to express behavioral correctness conditions like the validity of execution states, boundaries of variables or timing at a high level of abstraction and affirm that they are satisfied by a software system. However, this requires expressive models which are difficult and cumbersome to create and maintain by hand. This paper presents a framework that automatically derives behavioral models from real-sized Java programs. Our framework builds on the EMF/ECore technology and provides a tool that creates an initial model from Java bytecode, as well as a series of transformations that simplify the model and eventually output a timed-automata model that can be processed by a model checker such as UPPAAL. The framework has the following properties: (1) consistency of models with software, (2) extensibility of the model derivation process, (3) scalability and (4) expressiveness of models. We report several case studies to validate how our framework satisfies these properties.
AB - Model-based verification allows to express behavioral correctness conditions like the validity of execution states, boundaries of variables or timing at a high level of abstraction and affirm that they are satisfied by a software system. However, this requires expressive models which are difficult and cumbersome to create and maintain by hand. This paper presents a framework that automatically derives behavioral models from real-sized Java programs. Our framework builds on the EMF/ECore technology and provides a tool that creates an initial model from Java bytecode, as well as a series of transformations that simplify the model and eventually output a timed-automata model that can be processed by a model checker such as UPPAAL. The framework has the following properties: (1) consistency of models with software, (2) extensibility of the model derivation process, (3) scalability and (4) expressiveness of models. We report several case studies to validate how our framework satisfies these properties.
KW - Model Driven Engineering
KW - Metamodelling
KW - Model Transformaton
KW - Java bytecode
KW - UPPAAL
U2 - 10.4204/EPTCS.244.9
DO - 10.4204/EPTCS.244.9
M3 - Conference contribution
T3 - EPTCS - Electronic Publications in Theoretical Computer Science
SP - 217
EP - 229
BT - Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS)
A2 - Hermanns, Holger
A2 - Höffner, Peter
PB - arXiv.org
ER -