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]...

• Type: Conference
• Year: 2009
• Where: SIGSOFT
• Authors: Esteban Pavese, Sebastián Uchitel, Víctor A. Braberman
• Keywords: Model Checking, Probabilistic Automata-based Formalisms, Quantitative Model Checking, SIGSOFT 2009, Software Engineering