Friday 29th of March 2024
 

A Compact Semantic Model for Characterization of Stochastic Temporal Properties of Concurrent Systems


Mokdad Arous, Jean-Michel Ilié and Djamel-Eddine Saïdouni

In this paper, a new semantic model is proposed for characterizing the performance properties of stochastic concurrent systems, called Maximality-based Labeled Stochastic Transition System (MLSTS). A Stochastic Process Algebra, called S-LOTOS, is associated with these MLSTS models as a specification language to describe the stochastic temporal aspects of concurrent systems under the assumption of generally distributed durations of actions. The MLSTS models can be automatically generated from S-LOTOS specifications according to the (true concurrency) maximality semantics. In addition, we bring out the main advantage of the MLSTS as it is shown on practical examples in reducing the number of states and transitions w.r.t. standard ST-semantic models, which are frequently used in specification and modeling of stochastic systems with non-Markovian Process Algebra. Using our MoVeS Tool, we bring out the main advantage of our approach which is a drastic reduction obtained in the number of states and transitions, in comparison to standard ST-semantic models.

Keywords: Maximality Semantics, Semantic Models, ST-Semantics, Stochastic (non-Markovian) Process Algebra, Stochastic Transition Systems

Download Full-Text


ABOUT THE AUTHORS

Mokdad Arous
Mokdad AROUS graduated in Computer Science at the University of Mentouri of Constantine, Algeria, and he obtained his BEng degree in June 2003, and his MSc degree in June 2007. Currently, he is Assist Professor at the University of Souk-Ahras (Algeria), and he prepares his PhD thesis in computer science at the MISC Laboratory (Laboratoire de Modélisation et Implémentation des Systèmes Complexes) of University of Mentouri of Constantine, Algeria. His research interests are in the area of formal specification, verification and performance evaluation of stochastic concurrent systems.

Jean-Michel Ilié
Jean-Michel Ilié obtained several degrees in electronics and informatics among with its PhD thesis from the UPMC University of Paris (1990). The fields of his research concern the formal verification and validation of complex embedded systems. He received a special award as a co-author of the best paper for QEST 05 and contributes to four international books dedicated to its research domains.

Djamel-Eddine Saïdouni
Djamel Eddine Saidouni was born in Algeria in 1968. In 1996, he received his PHD degree in theoretical computer science from the university Paul Sabatier of Toulouse, France. Actually he is a professor at the department of computer science of Mentouri University of Constantine, Algeria. Also, he is the head of the CFSC research group of MISC laboratory. His main research domain interests formal models for specifying and verifying critical systems, real time systems, true concurrency models and state space explosion problem.


IJCSI Published Papers Indexed By:

 

 

 

 
+++
About IJCSI

IJCSI is a refereed open access international journal for scientific papers dealing in all areas of computer science research...

Learn more »
Join Us
FAQs

Read the most frequently asked questions about IJCSI.

Frequently Asked Questions (FAQs) »
Get in touch

Phone: +230 911 5482
Email: info@ijcsi.org

More contact details »