Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(7)
Composition Operator
Model Checking
Probabilistic Automata
Probabilistic Model
Probabilistic System
Probability of Error
Quantitative Analysis
Related Publications
(1)
A Model for Prob...
Subscribe
Academic
Publications
Probabilistic environments in the quantitative analysis of (nonprobabilistic) behaviour models
Probabilistic environments in the quantitative analysis of (nonprobabilistic) behaviour models,10.1145/1595696.1595760,Esteban Pavese,Víctor A. Brabe
Edit
Probabilistic environments in the quantitative analysis of (nonprobabilistic) behaviour models
(
Citations: 4
)
BibTex

RIS

RefWorks
Download
Esteban Pavese
,
Víctor A. Braberman
,
Sebastián Uchitel
System specifications have long been expressed through automatabased 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 nonprobabilistic system models by composing them with probabilistic models of the environment. Although many probabilistic automatabased 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 nonprobabilistic model of the systemunderanalysis.
Conference:
European Software Engineering Conference  ESEC
, pp. 335344, 2009
DOI:
10.1145/1595696.1595760
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.
(
portal.acm.org
)
(
portal.acm.org
)
(
doi.acm.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(4)
...In [
41
], Pavese et al. propose a quantitative analysis of nonprobabilistic models using probabilistic environments...
Benoît Delahaye
,
et al.
Probabilistic contracts: a compositional reasoning methodology for the...
...Also relevant are: [9], which presents an assume/guarantee framework using probabilistic contracts for nonprobabilistic 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 nonprobabilistic components...
Marta Z. Kwiatkowska
,
et al.
AssumeGuarantee 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 nonprobabilistic 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 Pavese
,
et 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 Krka
,
et al.
Probabilistic automata for architecturebased reliability assessment
References
(20)
It Usually Works: The Temporal Logic of Stochastic Systems
(
Citations: 98
)
Adnan Aziz
,
Vigyan Singhal
,
Felice Balarin
,
Robert Brayton
,
Alberto SangiovanniVincentelli
Conference:
Computer Aided Verification  CAV
, pp. 155165, 1995
A UserOriented Software Reliability Model
(
Citations: 198
)
Roger C. Cheung
Journal:
IEEE Transactions on Software Engineering  TSE
, vol. 6, no. 2, pp. 118125, 1980
Testing Equivalences and Fully Abstract Models for Probabilistic Processes
(
Citations: 56
)
Ivan Christoff
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 126140, 1990
Model Cheking
(
Citations: 4031
)
Edmund M. Clarke
Conference:
Foundations of Software Technology and Theoretical Computer Science  FSTTCS
, pp. 5456, 1997
On Generative Parallel Composition
(
Citations: 45
)
Pedro R. D'argenio
,
Holger Hermanns
,
Joostpieter Katoen
,
Christel Baier
,
Michael Huth
,
Marta Kwiatkowska
,
Mark Ryan
Journal:
Bulletin of The European Association for Theoretical Computer Science  EATCS
, vol. 22, 1999
Sort by:
Citations
(4)
Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or nondeterministic aspects
Benoît Delahaye
,
Benoît Caillaud
,
Axel Legay
Journal:
Formal Methods in System Design  FMSD
, vol. 38, no. 1, pp. 132, 2011
AssumeGuarantee Verification for Probabilistic Systems
(
Citations: 12
)
Marta Z. Kwiatkowska
,
Gethin Norman
,
David Parker
,
Hongyang Qu
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 2337, 2010
My model checker died!: how well did it do?
(
Citations: 1
)
Esteban Pavese
,
Víctor Braberman
,
Sebastian Uchitel
Published in 2010.
Probabilistic automata for architecturebased reliability assessment
Ivo Krka
,
Leana Golubchik
,
Nenad Medvidovic
Published in 2010.