Forschung

Design of Computer and Communication Systems

A research group within the Department of Computer Engineering (Technische Informatik) at the University of the Federal Armed Forces Munich. Group members are:

 

Overview

The group develops techniques and tools to support the design and analysis of computer and communication systems. The focus is on model-based performance and dependability evaluation of such systems, working with stochastic models which are specified with the help of stochastic process algebra, stochastic Petri nets, or related formalisms. We are working on the specification and automatic verification of  complex performability requirements. Furthermore, we are also interested in measurement-based evaluation and the integration of measurement and modelling.

Projects / Cooperations

We are currently conducting the DFG-sponsored project "Efficient Analysis Algorithms for Performability-Evaluation of Distributed Systems".  A previous DFG-sponsored project was PerformVER, where we developed highly expressive logics for formally specifying complex performability properties of concurrent systems. We devised efficient algorithms for symbolic model checking, and implementedd them in prototype software tools. Prior to this, we conducted two other DFG-sponsered projects: BDDana, which investigated efficient performance analysis on the basis of BDDs, and AutoVer, where we investigated the automatic verification of quality of service requirements of distributed systems. We cooperate, among others,

  • with the Universities of Aachen, Dresden, Nijmegen, Saarbrücken and Twente, supported by the DFG-NWO-sponsored project ROCKS.
  • with the Technical University of Munich, supported by the DFG-sponsored project "Model-based Dependability Analysis of Complex Fault-Tolerant Systems".
  • with the Universities of Aachen, Bonn, Nijmegen, Saarbrücken and Twente, supported by the DFG-NWO-sponsored project VOSS (completed).
  • with the Universities of Birmingham and Edinburgh, a collaboration originally supported by the DAAD project StochVer (completed).
  • with the the University of Illinois at Urbana-Champaign and the University of Cape Town.

Specification Language and Toolset for Reconfigurable Dependable Systems

For bridging the gap between high-level formalisms and formal modelling languages, the LAnguage for REconfigurable dependable Systems (LARES) has been defined [WGRSS09, RS12, GRS13, GGRSS09]. LARES provides means for hierarchical modelling, i.e. it separates between the definition of structure and behaviour and introduces scopes to restrict visibility of definitions. The formal semantics of LARES is defined either by means of flat labelled Markov chains or by stochastic process algebra (CASPA, see below). The LARES website is a resource for the LARES specification, tutorials on modelling and analysis using the LARES IDE, links to example models and news on current developments.

Representation and analysis of large Markov chains

In many areas of system design and analysis, there is the need to generate, manipulate and analyse very large state spaces. State space explosion is a serious problem when modelling parallel and distributed systems, because of the memory limitations of the available computing equipment.

We are working on the symbolic representation of large labelled CTMCs based on binary decision diagrams (BDD) and extensions thereof. We use multi-terminal BDDs (MTBDD) known from literature, decision-node BDDs (DNBDD) developed by ourselves, and more recently partially shared zero-suppressed MTBDDs (pZDD) [S02, LS06a]. In the presence of structured models which are composed of interacting submodels, the symbolic approach leads to provably compact representations of huge state spaces [HKNPS03]. For arbitrary models without any particular structure, the so-called activity-local scheme [LS03, LS06a] generates the state graph and processes reward-related information in a manner that is highly runtime- and memory-efficient.

Numerical analysis methods have successfully been adapted to the ZDDdata structure [LS06b], a work that is currently being extended.

We have developed several prototypical tools for BDD-based model generation, manipulation and analysis. Originally we used TIPPtool as a front end, but now our tool CASPA [KSW04] is a powerful stand-alone stochastic process algebra tool based entirely on symbolic data structures. One of our current activities concerns the integration of symbolic techniques into the multi-formalism modelling tool Möbius  which has led, among other results, to the implementation of an AFI for state-level objects represented by ZDDs.

Model checking of stochastic systems

We developed the action-based logic aCSL [HKMS00] for model checking action-labelled Markov chains stemming from stochastic process algebra specifications. More recently, we have been working on logics which extend the combined expressivity of CSL and aCSL by specifying arbitrarily complex execution paths which are characterised by regular expressions of actions and so-called tests. Two logics resulting from this work are sPDL [KS03, KS06] and asCSL [BCHKS04].

We developed the model checker ETMCC which enables its user to check properties against labelled continuous time Markov chains, where Continuous Stochastic Logic (CSL) and action-based CSL (aCSL) are used as the basic requirements specification languages [HKMS03]. In addition to CTL-type model checking algorithms, ETMCC includes sophisticated numerical analysis techniques which enable the tool to answer such questions as:

"Is the probability, that the sending of a message will be confirmed by an acknowledgement within 50 ms, at least 95%?".

ETMCC is based on sparse data structures, entirely written in Java (it runs on all Java1.2 enabled operating systems) and can be downloaded from the ETMCC homepage.