Encoding CDEVS and PDEVS into Timed Petri Net
Codage de CDEVS et de PDEVS en réseau de Petri temporisé
Résumé
This paper presents an encoding of CDEVS (Clas-sic Discrete-EVent Specification) and PDEVS (Parallel Discrete-EVent Specification) semantics in TPN (Timed Petri Nets) with priorities and data handling. This encoding is a formal specification of the execution semantics for our simulation tool. From a Timed Petri Net based model resulting from an automatic transformation of a DEVS model designed in ProDEVS, we perform an exhaustive exploration of the model. We show how to check formal verification simulation properties related to the correctness of the model : is it well built and legitimate for all its potential uses ? Will be properly executed by the simulator.
Cet article présente un codage des sémantiques CDEVS (Classic Discrete-EVent Specification) et PDEVS (Parallel Discrete-EVent Specification) en TPN (réseaux de Petri temporisés-Timed PetriNet) avec priorités et gestion des données. Ce codage constitue une spécification formelle de la sémantique d'exécution des modèles CDEVS et PDEVS pour notre outil de simulation ProDEVS [1]. A partir d'un modèlè a base de réseau de Petri résultant d'une transformation automatique d'un modèle DEVS saisi dans ProDEVS, nous exécutons une exploration exhaustive du modèle. Nous montrons comment faire une vérification formelle de propriétés de simulation liéesliées`liéesà la correction du modèle : est-il bien construit et légitime pour toutes seséventuelles ses´seséventuelles utilisations ? Sera-t-il correctement exécuté par le simulateur.
Domaines
Informatique [cs]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...