Title: Performance evaluation of stochastic real-time systems with the SBIP framework

Authors: Ayoub Nouri; Braham Lotfi Mediouni; Marius Bozga; Jacques Combaz; Saddek Bensalem; Axel Legay

Addresses: CNRS, Grenoble INP (Institute of Engineering), University Grenoble Alpes, VERIMAG, 38000 Grenoble, France ' CNRS, Grenoble INP (Institute of Engineering), University Grenoble Alpes, VERIMAG, 38000 Grenoble, France ' CNRS, Grenoble INP (Institute of Engineering), University Grenoble Alpes, VERIMAG, 38000 Grenoble, France ' CNRS, Grenoble INP (Institute of Engineering), University Grenoble Alpes, VERIMAG, 38000 Grenoble, France ' CNRS, Grenoble INP (Institute of Engineering), University Grenoble Alpes, VERIMAG, 38000 Grenoble, France ' INRIA Bretagne Atlantique, Campus de Beaulieu, 35042 Rennes, France

Abstract: The SBIP framework consists of a stochastic real-time component-based modelling formalism and a statistical model checking engine. The former is built as a stochastic extension of the real-time BIP formalism and enables the construction of stochastic real-time systems in a compositional way. The statistical engine implements a set of statistical algorithms for the quantitative and qualitative assessment of probabilistic properties. The paper provides a thorough introduction to the SBIP formalism and the associated verification method. In a second part, it surveys several case studies about modelling and verification of real-life systems, including various network protocols and multimedia applications.

Keywords: stochastic systems; real-time; component-based; formal models; generalised semi-Markov process; GSMP; behaviour interaction priority; BIP; statistical model checking; SMC; performance evaluation.

DOI: 10.1504/IJCCBS.2018.096439

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.3/4, pp.340 - 370

Received: 11 Sep 2017
Accepted: 21 May 2018
Published online: 30 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article