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

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

    Research output: Book/ReportReportProfessional

    73 Downloads (Pure)

    Abstract

    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 languageUndefined
    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)
    No.TR-CTIT-15-08
    ISSN (Print)1381-3625

    Keywords

    • IR-98885
    • METIS-315118
    • SE-MC: Model Checking
    • SE-MDA: Model Driven Architecture
    • CR-C.4
    • CR-I.6.5
    • EWI-26622
    • model-driven software engineering
    • Timing analysis
    • Model Transformation
    • Model Checking
    • Automatic model derivation

    Cite this

    Yildiz, B. M., Rensink, A., Bockisch, C., & Aksit, M. (2015). A Model-Derivation Framework for Timing Analysis of Java Software Systems. (CTIT Technical Report Series; No. TR-CTIT-15-08). Enschede: Centre for Telematics and Information Technology (CTIT).