AMETIST First Year: University of Twente

The UT prepared the following papers during the first year of the Ametist project.
A list of Bibtex entries for these publications is also available.

WP 1 Modelling

Quantitative Modelling

H. Hermanns and U. Herzog and J-P. Katoen.
Process algebra for performance evaluation.

This paper surveys the theoretical developments in the field of stochastic process algebras, process algebras where action occurrences may be subject to a delay that is determined by a random variable. A huge class of resource-sharing systems --- like large-scale computers, client-server architectures, networks --- can accurately be described using such stochastic specification formalisms.
The main emphasis of this paper is the treatment of operational semantics, notions of equivalence, and (sound and complete) axiomatisations of these equivalences for different types of Markovian process algebras, where delays are governed by exponential distributions. Starting from a simple action-less algebra for describing time-homogeneous continuous-time Markov chains, we consider the integration of actions and random delays both as a single entity (like in known Markovian process algebras like TIPP, PEPA and EMPA) and as separate entities (like in the timed process algebras timed CSP and TCCS). In total we consider four related calculi and investigate their relationship to existing Markovian process algebras. We also briefly indicate how one can profit from the separation of time and actions when incorporation more general, non-Markovian distributions.

In: Theoretical Computer Science, Vol. 274, Issue: 1-2, pages: 43 - 86, published in 2002.

H. Bohnenkamp and H. Hermanns and J.-P. Katoen and R. Klaren.
The MoDeST modeling tool and its implementation.

MoDeST is a modeling language that has a stochastic process algebra core and incorporates several ingredients from light-weight notations such as exception handling and data modularization. Its formal semantics provides a solid basis for the development of tool support whereas the light-weight ingredients pave the migration path toward system engineers. This paper presents the tool-suite MOTOR that supports the modeling and analysis of MoDeST specifications. In particular, we discuss its tool architecture, the parser, the SOS implementation, an interactive simulator, and the state-space generator. As the expressiveness of MoDeST goes beyond existing notations for real-time as well as probabilistic systems, the implementation of these tool components has a non-trivial intrinsic complexity.

Submitted to Performance Tools 2003, Urbana-Champaign, USA, 2003.

Hubert Garavel, Holger Hermanns
On Combining Functional Verification and Performance Evaluation using CADP.

Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.

Proceedings of the 11th International Symposium of Formal Methods Europe FME'2002 (Copenhagen, Denmark), July 2002. Full version available as INRIA Research Report RR-4492.

Holger Hermanns and Christophe Joubert.
A Set of Performance and Dependability Analysis Components for CADP.

This paper describes a set of analysis components that open the way to perform performance and dependability analysis with the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications. Three new tools (named BCG_STEADY, BCG_TRANSIENT, and DETERMINATOR) have been added to the toolbox. The approach taken fits well within the existing architecture of CADP, which doesn't need to be altered to enable performance evaluation.

Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland), April 2003

WP2 Analysis and Tools

Abstraction and Compositionality

Rom Langerak and Jan Willem Polderman and Tomas Krilavicius
Stability Analysis for Hybrid Automata Using Conservative Gains

This paper presents a stability analysis approach for a class of hybrid automata. It is assumed that the dynamics in each location of the hybrid automaton is linear and asymptotically stable, and that the guards on the transitions are hyperplanes in the state space. For each pair of ingoing and outgoing transitions in a location a conservative estimate is made of the gain via a Lyapunov function for the dynamics in that location. It is shown how the choice of the Lyapunov function can be optimized to obtain the best possible estimate. The calculated conservative gains are used in defining a so-called gain automaton that forms the basis of an algorithmic criterion for the stability of the hybrid automaton

IFAC Conference on Analysis and Design of Hybrid Systems (Submitted), Saint Malo, France, published in 2003

Rom Langerak and Jan Willem Polderman and Tomas Krilavicius
Stability Analysis For Hybrid Automata Using Optimal Lyapunov Functions
Accepted to International Conference on Dynamical Systems Modeling and Stability Investigation, May 27-30, 2003, Kyiv, Ukraine

Controller Synthesis and Scheduling Algorithms

Ed Brinksma, Angelika Mader.
Model checking embedded system designs.

The paper given an overview of the use of model checking techniques for scheduling verification, optimization, and synthesis.

Publication: WODES 2002 Invited Presentation.

Stochastic Techniques

B. Haverkort and L. Cloth and H. Hermanns and J.-P. Katoen and C. Baier.
Model-checking performability properties

Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system.
In recent years, we have extended CTL such that it allows for the specification of properties over finite-state continuous-time Markov chains (CTMCs). Computational techniques for model checking have been developed and successfully applied in the dependability context. Further work in this area has recently led to the continuous stochastic reward logic (CSRL), a logic to specify measures over CTMCs extended with a reward structure (so-called Markov reward models). Well-known performability measures, most notably also Meyer's performability distribution, can be easily defined with CSRL. However, using CSRL it is possible to specify performability measures that have not yet been addressed in the literature, hence, for which no computational procedures have been developed yet.
In this paper we present a number of computational procedures to perform model checking of CSRL over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.

In: International IEEE Conference on Dependable Systems and Networks (DSN), IEEE CS Press, Washington (D.C.), USA, pages: 103 - 112, published in 2002.

C. Baier and J.-P. Katoen and H. Hermanns and B. Haverkort.
Simulation for continuous-time Markov chains

This paper presents a simulation preorder for continuous-time Markov chains (CTMCs).
The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains.
The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

In: Concurrency Theory (CONCUR), Lecture Notes in Computer Science, Vol. 2421, Springer, Brno, Czech Republic, pages: 338 - 352, published in 2002.

H. Hermanns and J.-P. Katoen and J. Meyer-Kayser and M. Siegle.
A tool for model-checking Markov chains.

Markov chains are widely used in the context of performance and reliability modeling of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete and the continuous time setting. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen--Twente Markov Chain Checker (ETMCC), where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of the tool.

In: Int. Journal on Software Tools for Technology Transfer, Vol. 4, Issue: 2, pages: 153 - 172, published in 2003.

C. Baier and B. Haverkort and H. Hermanns and J.-P. Katoen.
Model-checking algorithms for continuous-time Markov chains

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al., contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

In: IEEE Transactions on Software Engineering, vol. 7, published in 2003 (to appear).

Henrik Bohnenkamp, Peter van der Stok, Holger Hermanns, Frits Vaandrager. Cost-Optimization of the IPv4 Zeroconf Protocol.

This paper investigates the tradeoff between reliability and effectiveness for the IPv4 Zeroconf protocol, proposed by Cheshire/Adoba/Guttman in 2002, dedicated to the self-configuration of IP network interfaces. We develop a simple stochastic cost model of the protocol, where reliability is measured in terms of the probability to avoid an address collision after configuration, while effectiveness is viewed as the average penalty perceived by a user. We derive an analytical expression for the user penalty which we use to derive optimal configuration parameters of the network, restricting to those parameters which are under the control of a consumer electronics manufacturer. In particular we show that minimal cost and maximal reliability are qualities that cannot be achieved at the same time.

International Conference on Dependable Systems and Networks (DSN'03)

Conrado Daws, Marta Kwiatkowska and Gethin Norman.
Automatic Verification of the IEEE-1394 Root Contention Protocol with Kronos and Prism

We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model-checker Kronos and the probabilistic model-checker Prism. The system is modelled as a probabilistic timed automaton. We first use Kronos to perform a symbolic forward reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state, and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with Prism. We apply this technique to compute the minimal probability of a leader being elected before a deadline, for different deadlines, and study the influence on this minimal probability, of using a biased coin, and considering different wire lengths.

Submitted to Int. Journal on Software Tools for Technology Transfer.

WP3 Case Studies

CS1: Smart Card Personalization System

Angelika Mader
Deriving Schedules for the Cybernetix Case Study

In this paper we show our first results on the Cybernetix case study within the AMETIST project. The point of investigation is to find (close) optimal schedules for a smart card personalisation system. After first, straightforward model checking techniques for derivation of schedules did not scale up we chose to follow a mixed strategy approach. The pure personalisation part was isolated, and with basic argumentation we showed optimality for two suggested schedules (under certain conditions). In the following we composed the graphical part to the personalisation part, and, by means of model checking, we investigated the throughput of the whole system assuming that personalisation part of the system is scheduled according to the earlier suggested strategies.

Theo C. Ruys
Optimal Scheduling using Branch and Bound with SPIN 4.0

The use of model checkers to solve discrete optimisation problems is appealing. A model checker can first be used to verify that the model of the problem is correct. Subsequently, the same model can be used to find an optimal solution for the problem. This paper describes how to apply the new Promela primitives of SPIN 4.0 to search effectively for the optimal solution. We show how Branch-and-Bound techniques can be added to the LTL property that is used to find the solution. The LTL property is dynamically changed during the verification.
We also show how the syntactical reordering of statements and/or processes in the Promela model can improve the search even further.
The techniques are illustrated using two running examples: the Travelling Salesman Problem and a job-shop scheduling problem.

The article will be presented at: Model Checking Software, 10th International SPIN Workshop, Portland, OR, USA, May 9-10, 2003. Editors: T. Ball and S.K. Rajamani. LNCS 2648, Springer-Verlag.

CS3: Real-time Service Allocation for Car Periphery Supervision

B. Gebremichael, H.Hermanns, T. Krilavicius, Y.Usenko.
Hybrid Modeling of a Vehicle Surveillance System with Real-Time Data Processing

Accepted for International Conference on Dynamical Systems Modeling and Stability Investigation, May 27-30, 2003, Kyiv, Ukraine

B. Gebremichael, T. Krilavicius, Y.Usenko.
Real-Time Service Allocation for Car Periphery Supervision: Requirements and Environment Analysis

Description of the requirements for the Car Periphery Supervision system designed by Bosch, and preliminary analysis of the environment relevant to how the system should operate.

B. Gebremichael, T. Krilavicius, Y.Usenko.
Formal Model of Car Periphery Supervision (CPS) System- BOSCH GmbH /AMETIST case study.

We present a formal model of the real-time service allocation for Car Periphery Supervision (CPS), a case study that has been proposed by Robert Bosch GmbH in the context of the EU IST project AMETIST. Despite the fact that the CPS system is a hybrid system with some probabilistic behavior, we model the system as timed automata without losing the key characteristics of the system. Our work is based on the papers provided by Robert BOSCH GmbH and visit to the CPS group in Frankfurt.

CS4: Value Chain Optimisation System

Angelika Mader
Axxom case study: a systematic modelling approach with timed automata

We report on the first steps in modelling a case study provided by AXXOM. The case study is a value chain management problem, where production of different types of lacquer for a number of different orders causes costs for, e.g., change of machines used or delay. The intention is to approach the related optimization problem with prized timed automata. Here, we focus on a clear derivation of a timed automaton model that makes the design steps explicit. As a first step we present the timed automaton models for three basic production flows. Systematic and explicit modelling is prerequesite for a (later) interpretation and comparison of results.