A Model-Derivation Framework for Timing Analysis of Java Software Systems

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

    Research output: Book/ReportReportProfessional

    145 Downloads (Pure)


    One of the main challenges in developing a software system is to assure that its properties fulfill the specifications. In the context of this paper, we are especially interested in timing properties. Model-based software verification is one of the approaches to achieve this. However, model-based verification requires expressive models of software systems and deriving such models is not a trivial task. Although there are a few model derivation tool proposals for the purpose of model-checking timing properties, these are dedicated tools supporting a selected set of verification techniques and as such they are not explicitly designed for coping with new demands. This paper presents a framework that derives models from Java programs in an automated way for analyzing timing properties. The framework has the following properties that are not provided by the previous proposals: (1) Efficiency in model development, (2) consistency of models with software, (3) expressiveness of models, (4) scalability and (5) extensibility of the model derivation process.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages26
    Publication statusPublished - 30 Dec 2015

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    ISSN (Print)1381-3625


    • SE-MC: Model Checking
    • SE-MDA: Model Driven Architecture
    • CR-C.4
    • CR-I.6.5
    • Model-driven software engineering
    • Timing analysis
    • Model transformation
    • Model checking
    • Automatic model derivation


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

    Cite this