QTDDS: Quantitative Techniques for Dependable Distributed Systems

The current state of technology requires that computing systems deliver services that can justifiably be trusted. Theses type of systems are said to be dependable and they are required to provide services that are available (i.e. the system is ready to provide a correct service), reliable (i.e. the system continuously provide a correct service), safe (i.e. the service is provided without catastrophic consequences), and secure (i.e. the service is provided confidentially to authorized users only while keeping the integrity of the data). Many times, these characteristics can only be stated via quantified measures. Examples of these properties are “connection is established 95% of the time” (availability), “97% of the transmitted messages are actually delivered”, “provided a failure occurs, the systems recovers with probability 0.99 within 5 minutes”, or “the probability of observing a given message is independent of the issuing agent”. (These are particular examples of quantitative properties describing availability, reliability, safety, and security, respectively.) In addition, properties can be stated with probability 1 on systems that by nature behave probabilistic, such as “the termination of a randomized leader election protocol is guaranteed to terminate with probability 1”.

We are interested in studying the specification and analysis of such kinds of quantitative properties, for systems that are concurrent, distributed, and/or with real-time characteristics. Prominent example application areas are wireless protocols and embedded systems. A ma jor issue for these types of systems is that activities are running loosely coupled in different components. As such, the system behaviour is inherently non-deterministic. As a consequence, non-deterministic activity and activity quantified through probabilities coexist, and must be considered together when reasoning about such systems.

In this cooperation we aim to study and develop foundations and techniques for the specification and analysis of distributed systems where execution branches are partially specified with probabilities.

This is a mobility project funded by MinCyT (AR) and DAAD (DE). It started in 2009 and lasted 2 years.

Participant Teams

• Dependable Systems and Software (Saarland University)
• Algebraic and Logical Foundations of Computer Science (TU Dresden)
• Software Modeling and Verification (RWTH Aachen)
• Dependable Systems Group (UNC)

Staff