Formal Approaches to Model-Driven Quality of Service
Energy Aware Networking Principles
Validation of Multiprocessor Multithreaded Architectures
Quantitative Model Checking of Software

Formal Approaches to Model-Driven Quality of Service

Design notations supporting quality of service (QoS) are needed to enable a seamless design flow with justifiable performance and other quantitative properties. This research challenge has inspired our work in several ways. Holger Hermanns has developed a compositional theory of interactive Markov chains (IMC) in which the principal models of functional verification and performance evaluation - transition systems and Markov chains - are semantically embedded. This provides the formal grounds for an integrated consideration of functional and performance properties in a single formalism. Holger Hermanns and coworkers have thus devised MoDeST, a language for concurrent, soft real-time systems. A dedicated webpage reports on the concept, the features, the applications and our own core activities related to MoDeST. Both formalisms, IMC and MoDeST serve as semantic vehicles for several of our QoS-related activities.



Recent achievements of the Dependable Systems and Software group in this context are:

  • StoCharts. Performance, dependability and QoS are prime aspects of the UML modelling domain. To capture these aspects effectively in a modelling language requires easy-to-use support for the specification and analysis of randomly varying behaviours. Already in a UML 2003 paper, David N. Jansen, Holger Hermanns and Joost-Pieter Katoen, have introduced StoCharts. StoCharts extend UML statecharts with randomly varying durations in a simple, elegant but very expressive way. StoCharts have been given a semantics in terms of MoDeST, in joint work of Holger Hermanns with David N. Jansen and Yaroslav S. Usenko. Recently, Christophe Boutter has implemented this semantics, as a preprocessor that rewrites StoCharts models, specified with a variant of the TCM tool into MoDeST code. This means that the MoDeST tool MoToR can be (and is) used as a back-end analysis engine for these UML models. See here for a case study performed with StoCharts and MoDeST.
  • Compositional Analysis of Dynamic Fault Trees. A DSN 2007 paper devises a compositional analysis method for dynamic fault trees. This is work by Pepijn Crouzen, jointly with Hichem Boudali and MariŽlle Stoelinga from University of Twente. The underlying model is a variation of interactive Markov chains (namely input/output interactive Markov chains), and therefore tool support developed inside the group is readily available for fault tree analysis. The use of input/output interactive Markov chains provides a very useful formal basis for dynamic fault trees. Furthermore it makes the DFT formalism more adaptable and more extensible. A number of case studies show that the compositional analysis approach can combat the state space explosion problem.
  • Compositional Performability Evaluation for STATEMATE. We are dedicating considerable efforts to link an industrial state-of-the-art modelling tool to academic state-of-the-art analysis algorithms. In a nutshell, we enable timed stochastic reachability analysis of stochastic models, which are generated from STATEMATE. This allows one to answer questions such as: "Is the risk to hit an unsafe system state within a mission time of X seconds smaller than Y" - on the basis of a STATEMATE model! The entire tool flow has been implemented, and is being applied to several nontrivial case studies and examples. This research is a joint initiative of the groups of Bernd Becker (Univ Freiburg), Werner Damm (Univ Oldenburg), and Holger Hermanns (Saarland Univ), as part of subproject S3 of the ''Sonderforschungsbereich'' SFB/TR-14 AVACS. The main reference is a joint publication in QEST 2006.
  • Uniformity by Construction.
  • A crucial step in the above connection of STATEMATE to timed stochastic reachability analysis is based on a quite technical, but quite important insight: The entire construction and analysis trajectory can be shown to preserve uniformity. This ensures that the results obtained by the S3 tool flow are correct in a very deep sense. The detailed aspects of uniformity are handled in a publication in DSN 2007, jointly by Holger Hermanns and Sven Johr. It is worthwhile to mention that the compositionality of the construction is inherited from that of interactive Markov chains , since the central model on which the whle analysis chain is grounded, is that of uniform interarctive Markov chains.