Modeling and Evaluation of Stochastic Discrete-Event Systems with RayLang Formalism

In recent years, formal methods have been used as an important tool forperformance evaluation and verification of a wide range of systems. In the viewpoints of engineers and practitioners, however, there are still some major difficultiesin using formal methods. In this paper, we introduce a new formal modelinglanguage to fill the gaps between object-oriented programming languages (OOPLs)used by engineers and the formalisms used for evaluation and verification purposes.We propose the syntax and semantics of a new object-oriented modeling languagefor discrete-event systems called RayLang. We have designed the syntax of RayLangsimilar to OOPLs. In RayLang models, objects that are instantiated from classes,run concurrently and can communicate with each other by requesting services.Every object in RayLang models has some internal state variables and some servicehandlers for executing the requests of other objects. We have shown that MarkovianRayLang models can be transformed into continuous-time Markov chains (CTMCs)and then can be solved by existing solution techniques. For modeling, discrete-eventsimulation and analytic solution of RayLang models, we have implemented thesemodels in the PDETool framework.

Keywords:

Formal Modeling Language , Object-Oriented Modeling , Discrete-Event Systems , Performance and Dependability Evaluation