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.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||26|
|Publication status||Published - 30 Dec 2015|
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|
- SE-MC: Model Checking
- SE-MDA: Model Driven Architecture
- model-driven software engineering
- Timing analysis
- Model Transformation
- Model Checking
- Automatic model derivation
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).