Skip to main content
Department of Information Technology
Speaker

Toshiaki Aoki

Date and Time

Thursday, September 23rd, 2010 at 15:15

Location

Polacksbacken, room 1145


Automatic Generation of Model Checking Scripts based on Environment Modeling

(expected duration: 20min)

Abstract

When applying model checking to the design models of the embedded systems, it is necessary to model not only the behavior of the target system but also that of the environment interacting with the system. In this talk, we present a method to model the environment and to automatically generate all possible environments from the model. In our method, we can flexibly model the structural variation of the environment and the sequences of the function calls using a class model and statechart models. We also present a tool to generate Promela scripts of SPIN from the environment model. As a practical experiment, we applied our tool to the verification of an OSEK/VDX RTOS design model.


Modeling of Real-Time System Designs for Parametric Analysis

(expected duration: 20min)

Abstract

In designing real-time software, system designers need to find out the time budget to allocate to each action of real-time tasks so that the tasks can meet their deadlines. Our solution to this problem involves representing the execution time of the actions as parameters, then analyzing the collaborative behavior of those real-time tasks. We proposes parametric timed models of real-time tasks whose executions are controlled by a scheduler. We develop an algorithm to synthesize a coherent model which represents the possible behavior from a set of real-time tasks by exhaustively searching their reachable states. A set of linear inequalities are then derived on the fly from the synthesized model as the condition of parameters for schedulability. By solving the inequalities using a constraint solver, we can obtain desirable values of the parameters. In addition, we have implemented the algorithm in a tool and conducted some experiments to show the effectiveness of our approach.

Back to the seminar page

Updated  2010-09-08 12:03:23 by Frédéric Haziza.