Transactions on Software Engineering

The IEEE Transactions on Software Engineering (TSE) is an archival journal published bimonthly. We are interested in well-defined theoretical results and empirical studies that have potential impact on the construction, analysis, or management of software. Read the full scope of TSE

Expand your horizons with Colloquium, a monthly survey of abstracts from all CS transactions! Replaces OnlinePlus in January 2017.

From the September 2016 Issue

Probabilistic Interface Automata

By Esteban Pavese, Victor Braberman, and Sebastian Uchitel

Featured article thumbnail imageSystem specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata.

download PDF View the PDF of this article      csdl View this issue in the digital library

Editorials and Announcements



Guest Editorials

Reviewers List

Annual Index

Access All Recently Published TSE Articles

RSS Subscribe to the RSS feed of latest TSE content added to the digital library

Mail Sign up to receive email alerts when a new issue of TSE is online.

Access TSE PrePrints in the Computer Society digital library

A PrePrint is an article that has been accepted for publication in a future issue of this journal, but has not been fully edited. Content may change prior to final publication