Academic
Publications
Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models

Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models,10.1145/1595696.1595760,Esteban Pavese,Víctor A. Brabe

Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models   (Citations: 4)
BibTex | RIS | RefWorks Download
System specifications have long been expressed through automata-based languages, enabling verification techniques such as model checking. These verification techniques can assess whether a property holds or not, given a system specification. Quantitative model checking can provide additional information on the probability of these properties holding. We are interested in quantitatively analysing the probability of errors in non-probabilistic system models by composing them with probabilistic models of the environment. Although many probabilistic automata-based formalisms and composition operators exist, these are not adequate for such a setting. In this work we present a formalism inspired on interface automata and a suitable composition operator for these automata that enables validation of environment models in isolation and sound analysis of its composition with the non-probabilistic model of the system-under-analysis.
Conference: European Software Engineering Conference - ESEC , pp. 335-344, 2009
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...In [41], Pavese et al. propose a quantitative analysis of non-probabilistic models using probabilistic environments...

    Benoît Delahayeet al. Probabilistic contracts: a compositional reasoning methodology for the...

    • ...Also relevant are: [9], which presents an assume/guarantee framework using probabilistic contracts for non-probabilistic models; [3], which presents a theoretical framework for compositional verication of quantitative (but not probabilistic) properties; and [17], which uses probabilistic automata to model the environment of non-probabilistic components...

    Marta Z. Kwiatkowskaet al. Assume-Guarantee Verification for Probabilistic Systems

    • ...We show how our ideas can be built on top of our previous results on composition of probabilistic environment behaviour models with non-probabilistic system models [15] and we illustrate our ideas with a running example...
    • ...In particular, we model these operational profiles via an automata based formalism, Probabilistic Interface Automata (PIA), that we have introduced in [15] and which is defined as follows...
    • ...The reader is referred to [15] for further details, complete definitions and motivations...
    • ...The reader is referred to [15] for insight into the theorem...
    • ...Although the basis for this underpinning, Probabilistic Interface Automata [15], has been studied, there are a number of theoretical results that need to be proved in order to complete the argument as to why the various compositions, partial explorations and measurements are sound...

    Esteban Paveseet al. My model checker died!: how well did it do?

    • ...To this end, we propose probabilistic component interface protocol, which is a novel probabilistic formalism that combines features of probabilistic IO automata [19] and probabilistic interface automata [13]...
    • ...We then present two probabilistic modeling formalisms that differentiate between controlled and uncontrolled actions: the probabilistic IO automata [19] and the probabilistic interface automata [13]...
    • ...Probabilistic interface automata [13], distinguish between input and output actions, while also explicitly modeling internal actions...
    • ...In our discussion, we utilize four techniques [1, 2, 13, 16] that are representative of the commonly applied modeling approaches...
    • ...Pavese et al. [13] adopt a converse viewpoint by exclusively considering the reliability impacts of a system’s probabilistic environment (the environment is represented with a probabilistic interface automaton)...
    • ...The probabilistic interface automata specification [13] proclaims the inconsistent composite state as illegal ;t he goal is then to create an environment that avoids the illegal state...

    Ivo Krkaet al. Probabilistic automata for architecture-based reliability assessment

Sort by: