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:



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 PerformVER, where we develop highly expressive logics for formally specifying complex performability properties of concurrent systems. We devise efficient algorithms for symbolic model checking, and implement 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, Bonn, Nijmegen, Saarbrücken and Twente, supported by the DFG-NWO-sponsored project VOSS.
  • with the Universities of Birmingham and Edinburgh, a collaboration originally supported by the DAAD project StochVer.
  • with the Technical University of Munich, the University of Illinois at Urbana-Champaign and the University of Cape Town.

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.