Advertisement
Published in:
2013 | OriginalPaper | Chapter
Towards an Integrated Specification and Analysis of Functional and Temporal Properties:
Part I: Functional Aspect Verification
Authors : Mokdad Arous, Djamel-Eddine Saïdouni
Published in: Modeling Approaches and Algorithms for Advanced Computer Applications
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Maximality-based Labeled Stochastic Transition Systems
(MLSTS) was presented [6, 11] as a new semantic model for characterizing the functional and performance properties of concurrent systems, under the assumption of arbitrarily distributed (i.e. non-Markovian) durations of actions. The MLSTS models can be automatically generated from S-LOTOS specifications according to the (true concurrency) maximality semantics [6]. The main advantage is to pruning the state graph without loss of information w.r.t. ST-semantic models [11]. As a first work on MLSTS, we focus in this paper on in the verification of functional properties of systems, using a variant of model-checking technique.