Modelling Parallel Stochastic-Time Systems Using Timed and Synchronous Layers : Introducing the Parallel Stochastic Timed State Machine

Abstract: In the development phase of real-world cyper-physical systems, modelling and analysis often plays a vital role. For instance, before a new system is produced and deployed, questions such as ‘what is the probability that the system will fail within its lifetime?’ must be answered. However, modelling formalisms suitable for continuous-time systems that behave stochastically cannot always represent parallelism in an accurate way. Moreover, they often su↵er from problems such as exponentially growing state spaces, intricately coupled transition diagrams and inflexible synchronisation semantics. In order to solve such shortcomings, this thesis introduces a new modelling formalism called the parallel stochastic timed state machine (PSTSM). It is especially suitable for systems that exhibit a modular nature where each module behaves similar to a semi-Markov process, and in such cases can serve as a more natural modelling tool than some popular existing formalisms with the same purpose. It utilises a multi-dimensional state space for explicitly handling parallelism and also allows the modeller to define custom synchronisation semantics in terms of a user-specified function. This enables the combination of several di↵erent semantics under the same uniform representation. Furthermore, methods for automatically generating such a function from well-known synchronisation constructs such as guards and events are presented. In order to analyse the produced models, a succession algebra is developed together with functions that enable looking at subsets of the parallel components separately. Nondeterministic and purely probabilistic cases of the models are explored and an algorithm for extracting the transition diagram of the underlying stochastic process is presented. The stochastic processes are furthermore categorised within well-known classes depending on the synchronisation patterns that the models exhibit.