Search

Non-functional properties, such as timeliness, resource consumption and reliability are of crucial importance for today’s software systems. Therefore, it is important to know the non-functional behavior before the system is put into operation. Preferably, such properties should be analyzed at design time, at an architectural level, so that changes can be made early in the system development process. In this paper, we present an efficient and easy-to-use methodology to predict – at design time – the availability of systems that support local recovery. Our analysis techniques work at the architectural level, where the software designer simply inputs the software modules’ decomposition annotated with failure and repair rates. From this decomposition we automatically generate an analytical model (i.e. a continuous-time Markov chain), from which various performance and dependability measures are then computed, in a way that is completely transparent to the user. A crucial step is the use of intermediate models in the Input/Output Interactive Markov Chain formalism, which makes our techniques, efficient, mathematically rigorous, and easy to adapt. In particular, we use aggressive minimization techniques to keep the size of the generated state spaces small. We have applied our methodology on a realistic case study, namely the MPlayer open source software. We have investigated four different decomposition alternatives and compared our analytical results with the measured availability on a running MPlayer. We found that our predicted results closely match the measured ones.

This paper discusses the requirements that a suitable formalism for dependability modeling/evaluation should possess. We also discuss the outline of Arcade, an architectural dependability formalism that we are developing.

This paper proposes a formally well-rooted and extensible framework for dependability evaluation: Arcade (architectural dependability evaluation). It has been designed to combine the strengths of previous approaches to the evaluation of dependability. A key feature is its formal semantics in terms of input/output-interactive Markov chains, which enables both compositional modeling and compositional state space generation and reduction. The latter enables great computational reductions for many models. The Arcade approach is extensible, hence adaptable to new circumstances or application areas. The paper introduces the new modeling approach, discusses its formal semantics and illustrates its use with two case studies.

This paper considers QLtl, a quantitative analagon of Ltl and presents algorithms for model checking QLtl over quantitative versions of Kripke structures and Markov chains.

We introduce a notion of finite testing, based on statistical hypothesis tests, via a variant of the well-known trace machine. Under this scenario, two processes are deemed observationally equivalent if they cannot be distinguished by any finite test. We consider processes modeled as image finite probabilistic automata and prove that our notion of observational equivalence coincides with the trace distribution equivalence proposed by Segala. Along the way, we give an explicit characterization of the set of probabilistic generalize the Approximation Induction Principle by defining an also prove limit and convex closure properties of trace distributions in an appropriate metric space.

We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal (e.g., “reach a target state��?), the question of winning is thus a probabilistic one: “what is the maximal probability of winning from a given state?��?. On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state “similarity��?. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative μ-calculus. The quantitative μ- calculus can express a large set of goals, including reachability, safety, and ω-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.

We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time.

We consider concurrent two-person games played in real time, in which the players decide both which action to play, and when to play it. Such timed games differ from untimed games in two essential ways. First, players can take each other by surprise, because actions are played with delays that cannot be anticipated by the opponent. Second, a player should not be able to win the game by preventing time from diverging. We present a model of timed games that preserves the element of surprise and accounts for time divergence in a way that treats both players symmetrically and applies to all ω-regular winning conditions. We prove that the ability to take each other by surprise adds extra power to the players. For the case that the games are specified in the style of timed automata, we provide symbolic algorithms for their solution with respect to all ω-regular winning conditions. We also show that for these timed games, memory strategies are more powerful than memoryless strategies already in the case of reachability objectives.

We present an extension of the model checker Uppaal capable of synthesizing linear parameter constraints for the correctness ofparametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second contribution of thispaper is the identification of a subclass of parametric timed automata(L/U automata), for which the emptiness problem is decidable, contraryto the full class where it is know to be undecidable. Also we present anumber of lemmas enabling the verification effort to be reduced for L/Uautomata in some cases. We illustrate our approach by deriving linearparameter constraints for a number of well-known case studies from theliterature (exhibiting a flaw in a published paper).

The model of probabilistic I/O automata of Segala and Lynch is used for the formal specification and analysis of the root contention protocol from the physical layer of the IEEE 1394 ("FireWire") standard. In our model of the protocol both randomization and real-time play an essential role. In order to make our verification easier to understand we introduce several intermediate automata in between the implementation and the specification automaton. This allows us to use very simple notions of refinement rather than the more general but also very complex simulation relations which have been proposed by Segala and Lynch.

Traditional type systems specify interfaces in terms of values and domains. When we apply a function to an argument, or when we compose two functions, we have to check that their types match. Interface models extend type systems with the ability to reason about the dynamic behavior of design components. For instance, interface models are able to capture temporal-ordering constraints on component interaction, such as constraints on the ordering of method calls or protocol messages, timing constraints on a component's input and output signals, and constraints on the usage of shared resources. Like type systems, interfaces specify both the input assumptions a component makes on its environment and the output guarantees it provides. Interfaces are based on two-player games in which the system plays against the environment. The moves of the environment (player Input) represent the inputs that the system can receive from the environment, that is, the input assumption of the system. Symmetrically, the moves of the system (player Output) represent the possible outputs that can be generated by the system. Interfaces are built around the concepts of (1) well-formedness, requiring that the input assumptions of an interface be satisfiable; (2) compatibility, asking whether two components can be used in a way that satisfies the input assumptions of both components; (3) composition of compatible interfaces; and (4) refinement, asking whether one component (being an implementation) correctly implements another one (being the specification). This paper provides a tutorial-style introduction to interfaces and discusses the basic concepts and ideas. In particular, we elaborate on the automaton-based interfaces from [L. de Alfaro and T.A. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109–120. ACM Press, 2001] and the timed interfaces from [L. de Alfaro, T.A. Henzinger, and M.I.A. Stoelinga. Timed interfaces. In Proceedings of the Second International Workshop on Embedded Software (EMSOFT 2002), volume 2491 of Lect. Notes in Comp. Sci., pages 108–122. Springer-Verlag, 2002]. Due space limitations, we do not treat the notion of interface refinement, but we refer the reader to [L. de Alfaro and T.A. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109–120. ACM Press, 2001] and [L. de Alfaro. Game models for open systems. In Int. Symposium on Verification celebrating Zohar Manna's 64th Birthday, volume 2772 of Lect. Notes in Comp. Sci. Springer-Verlag, 2003].

Confidentiality is an important concern in today’s informa- tion society: electronic payment and personal data should be protected appropriately. This holds in particular for multi-threaded applications, which are generally seen the future of high-performance computing. Multi- threading poses new challenges to data protection, in particular, data races may be exploited in security attacks. Also, the role of the sched- uler is seminal in the multi-threaded context. This paper proposes a new notion of confidentiality for probabilistic and non-probabilistic multi-threaded programs, formalized as scheduler- specific probabilistic observational determinism (SSPOD), together with verification methods. Essentially, SSPOD ensures that no information about the private data can be derived either from the public data, or from the probabilities of the public data being changed. Moreover, SS- POD explicitly depends on a given (class of) schedulers. Formally, this is expressed by using two conditions: (i) each publicly visible variable individually behaves deterministically with probability 1, and (ii) for every trace considering all publicly visible variables, there always exists a matching trace with equal probability. We verify these conditions by a clever combination of new and existing algorithms over probabilistic Kripke structures.

International audience; This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations, as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex to implement than refinement checking.