Courrier du Savoir scientifique et technique
Volume 14, Numéro 14, Pages 25-30
2014-05-07

From A Model Of Concurrency To A Test Model: A Graph Transformation Based Approach

Auteurs : Chaoui A . Saidouni D . Bouarioua M . Bekrar S . Kerkouche E .

Résumé

Maximality-based Labeled Transition Systems (MLTS) is semantic model for true concurrency. In other hand Mixed Refusal Graphs (MRG) are models for formal testing. In this paper, we propose an approach to transform an MLTS model to an equivalent MRG model. Since the input and output models are graphs, we use graph transformation to perform this transformation automatically. So, we propose two meta-models; one for the input model and the other for the output model. Then, based on these meta-models we propose a graph grammar that deals with the transformation process. The metamodeling tool ATOM3 is used. Our approach is illustrated through an example.

Mots clés

Formal Verification, Graph transformation, MLTS, MRG, ATOM3, Meta-models, Test model.