A Model-Derivation Framework for Software Analysis

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)
    162 Downloads (Pure)


    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.
    Original 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
    Publication statusPublished - 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

    Publication series

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


    Conference2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017
    Abbreviated titleMARS
    Internet address


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


    Dive into the research topics of 'A Model-Derivation Framework for Software Analysis'. Together they form a unique fingerprint.

    Cite this