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

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

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
StatePublished - 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

Fingerprint

Model checking
Scalability
Specifications

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).

Yildiz, Bugra Mehmet; Rensink, Arend; Bockisch, Christoph; Aksit, Mehmet / A Model-Derivation Framework for Timing Analysis of Java Software Systems.

Enschede : Centre for Telematics and Information Technology (CTIT), 2015. 26 p. (CTIT Technical Report Series; No. TR-CTIT-15-08).

Research output: ProfessionalReport

@book{47ea6c847db141a6946e200b61952e38,
title = "A Model-Derivation Framework for Timing Analysis of Java Software Systems",
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.",
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",
author = "Yildiz, {Bugra Mehmet} and Arend Rensink and Christoph Bockisch and Mehmet Aksit",
note = "eemcs-eprint-26622",
year = "2015",
month = "12",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-15-08",
address = "Netherlands",

}

Yildiz, BM, 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, Centre for Telematics and Information Technology (CTIT), Enschede.

A Model-Derivation Framework for Timing Analysis of Java Software Systems. / Yildiz, Bugra Mehmet; Rensink, Arend; Bockisch, Christoph; Aksit, Mehmet.

Enschede : Centre for Telematics and Information Technology (CTIT), 2015. 26 p. (CTIT Technical Report Series; No. TR-CTIT-15-08).

Research output: ProfessionalReport

TY - BOOK

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

AU - Yildiz,Bugra Mehmet

AU - Rensink,Arend

AU - Bockisch,Christoph

AU - Aksit,Mehmet

N1 - eemcs-eprint-26622

PY - 2015/12/30

Y1 - 2015/12/30

N2 - 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.

AB - 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.

KW - IR-98885

KW - METIS-315118

KW - SE-MC: Model Checking

KW - SE-MDA: Model Driven Architecture

KW - CR-C.4

KW - CR-I.6.5

KW - EWI-26622

KW - model-driven software engineering

KW - Timing analysis

KW - Model Transformation

KW - Model Checking

KW - Automatic model derivation

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Centre for Telematics and Information Technology (CTIT)

ER -

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