Sciweavers

Share
SIGSOFT
2009
ACM

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

9 years 7 months ago
Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models
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. Categories and Subject Descriptors D.2.1 [Software Engineering]...
Esteban Pavese, Sebastián Uchitel, Ví
Added 19 Nov 2009
Updated 19 Nov 2009
Type Conference
Year 2009
Where SIGSOFT
Authors Esteban Pavese, Sebastián Uchitel, Víctor A. Braberman
Comments (0)
books