A Model-Derivation Framework for Software Analysis

Bugra M. Yildiz, Arend Rensink, Christoph Bockisch, Mehmet Aksit

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1 Citations

Abstract

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.
LanguageEnglish
Title of host publicationProceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS)
Subtitle of host publicationUppsala, Sweden, 29th April 2017
EditorsHolger Hermanns, Peter Höffner
PublisherarXiv.org
Pages217-229
DOIs
StatePublished - Apr 2017
Event2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017 - Uppsala, Sweden
Duration: 29 Apr 201729 Apr 2017
Conference number: 2
http://mars-workshop.org/mars2017/

Publication series

NameEPTCS - Electronic Publications in Theoretical Computer Science
Volume244
ISSN (Print)2075-2180

Conference

Conference2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017
Abbreviated titleMARS
CountrySweden
CityUppsala
Period29/04/1729/04/17
Internet address

Fingerprint

Scalability
Electric potential

Keywords

  • Model Driven Engineering
  • Metamodelling
  • Model Transformaton
  • Java bytecode
  • UPPAAL

Cite this

Yildiz, B. M., Rensink, A., Bockisch, C., & Aksit, M. (2017). A Model-Derivation Framework for Software Analysis. In H. Hermanns, & P. Höffner (Eds.), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS): Uppsala, Sweden, 29th April 2017 (pp. 217-229). (EPTCS - Electronic Publications in Theoretical Computer Science; Vol. 244). arXiv.org. DOI: 10.4204/EPTCS.244.9
Yildiz, Bugra M. ; Rensink, Arend ; Bockisch, Christoph ; Aksit, Mehmet . / A Model-Derivation Framework for Software Analysis. Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS): Uppsala, Sweden, 29th April 2017. editor / Holger Hermanns ; Peter Höffner. arXiv.org, 2017. pp. 217-229 (EPTCS - Electronic Publications in Theoretical Computer Science).
@inproceedings{54563416650445548af775ca474aaaf1,
title = "A Model-Derivation Framework for Software Analysis",
abstract = "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.",
keywords = "Model Driven Engineering, Metamodelling, Model Transformaton, Java bytecode, UPPAAL",
author = "Yildiz, {Bugra M.} and Arend Rensink and Christoph Bockisch and Mehmet Aksit",
year = "2017",
month = "4",
doi = "10.4204/EPTCS.244.9",
language = "English",
series = "EPTCS - Electronic Publications in Theoretical Computer Science",
publisher = "arXiv.org",
pages = "217--229",
editor = "Holger Hermanns and Peter H{\"o}ffner",
booktitle = "Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS)",

}

Yildiz, BM, Rensink, A, Bockisch, C & Aksit, M 2017, A Model-Derivation Framework for Software Analysis. in H Hermanns & P Höffner (eds), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS): Uppsala, Sweden, 29th April 2017. EPTCS - Electronic Publications in Theoretical Computer Science, vol. 244, arXiv.org, pp. 217-229, 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017, Uppsala, Sweden, 29/04/17. DOI: 10.4204/EPTCS.244.9

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 proceedingConference contribution

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)

PB - arXiv.org

ER -

Yildiz BM, Rensink A, Bockisch C, Aksit M. A Model-Derivation Framework for Software Analysis. In Hermanns H, Höffner P, editors, Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS): Uppsala, Sweden, 29th April 2017. arXiv.org. 2017. p. 217-229. (EPTCS - Electronic Publications in Theoretical Computer Science). Available from, DOI: 10.4204/EPTCS.244.9