Probabilistic Interface Automata

ESTEBAN PAVESE; BRABERMAN VICTOR; UCHITEL SEBASTIAN

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

IEEE COMPUTER SOC

Lugar: Los Alamitos, CA, USA; Año: 2016

0098-5589

Abstract?System specifications have long been expressedthrough automata-based languages, which allow for compositionalconstruction of complex models and enable automatedverification techniques such as model checking. Automata-basedverification has been extensively used in the analysis of systems,where they are able to provide yes/no answers to queriesregarding their temporal properties. Probabilistic modelling andchecking aim at enriching this binary, qualitative informationwith quantitative information, more suitable to approaches suchas reliability engineering.Compositional construction of software specifications reducesthe specification effort, allowing the engineer to focus on specifyingindividual component behaviour to then analyse thecomposite system behaviour. Compositional construction alsoreduces the validation effort, since the validity of the compositespecification should be dependent on the validity of thecomponents. These component models are smaller and thuseasier to validate. Compositional construction poses additionalchallenges in a probabilistic setting. Numerical annotations ofprobabilistically independent events must be contrasted againstestimations or measurements, taking care of not compoundingthis quantification with exogenous factors, in particularthe behaviour of other system components. Thus, the validityof compositionally constructed system specifications requiresthat the validated probabilistic behaviour of each componentcontinues to be preserved in the composite system. However,existing probabilistic automata-based formalisms do not supportspecification of non-deterministic and probabilistic componentbehaviour which, when observed through logics such as pCTL,is preserved in the composite system.In this paper we present a probabilistic extension to InterfaceAutomata which preserves pCTL properties under probabilisticfairness by ensuring a probabilistic branching simulationbetween component and composite automata. The extensionnot only supports probabilistic behaviour but also allows forweaker prerequisites to interfacing composition, that supportsdelayed synchronisation that may be required because of internalcomponent behaviour. These results are equally applicable as anextension to non-probabilistic Interface Automata