A modest approach to practical formal methods

Holger Hermanns
Saarland University
Thursday, 8 March, 2007 (All day)

Stochastic timed systems and stochastic temporal logics have been proposed to express and check requiremnts like correctness, availability, survivability or performability of trustworthy real-time system designs. They are partially accompanied by model-checking algorithms which can be applied to certify these requirements on a component level.

This talk gives an overview of recent achievements in this area. It will detail the achieved results in two related areas: After introducing the mathematical background and context, I will report on our efforts to link an industrial modelling tool to academic state-of-the-art model-checking algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from STATEMATE models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible.

With a slightly broader perspective, I am then going to introduce MoDeST (MOdeling and DEscription language for Stochastic Timed systems), a formalism to support (i) the compositional description of reactive systems' behavior while covering both (ii) functional and (iii) nonfunctional system aspects such as timing and quality-of-service constraints in a single compositional specification. This unique expressiveness has been exploited in three recent industrial case studies of rather different nature, ranging from (i) schedule synthesis and evaluation for a lacquer production plant, to (ii) energy efficiency assesment of ZigBee devices, and to (iii) dependability assessment of an emerging standard for future high-speed cross-European trains.