Title: Formal testing theory of stochastic systems under maximality semantics

Authors: Kenza Bouaroudj; Djamel Eddine Saidouni; Ilhem Kitouni

Addresses: Department of Computer Science and its Application, MISC Laboratory, Faculty of New Technologies of Information and Communication, University Constantine 2, Constantine, 25000, Algeria ' Department of Computer Science and its Application, MISC Laboratory, Faculty of New Technologies of Information and Communication, University Constantine 2, Constantine, 25000, Algeria ' Department of Computer Science and its Application, MISC Laboratory, Faculty of New Technologies of Information and Communication, University Constantine 2, Constantine, 25000, Algeria

Abstract: This paper introduces an approach for testing stochastic systems based on stochastic refusals graphs (SRGs). Those systems are modelled by maximality-based labelled stochastic transition systems (MLSTSs). This model characterises the stochastic temporal properties of concurrent systems, under the assumption of arbitrarily distributed durations of actions. In this paper, we propose a theory and a framework for the determinisation of MLSTS and a definition of canonical tester. This theory is applied on stochastic process algebra S-LOTOS. At the end, this theory will be illustrated by three case studies; temperature controller of plane reactor, alternating bit protocol and cell production.

Keywords: maximality semantics; maximality-based labelled stochastic transition system; MLSTS; refusal graphs; canonical tester; formal testing theory; stochastic systems; modelling; temperature controllers; plane reactors; alternating bit protocol; cell production.

DOI: 10.1504/IJCAET.2015.071296

International Journal of Computer Aided Engineering and Technology, 2015 Vol.7 No.3, pp.348 - 377

Received: 24 May 2013
Accepted: 12 Nov 2013
Published online: 20 Aug 2015 *

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