Encoding CDEVS and PDEVS into Timed Petri Net

Autor: Albert, Vincent, Ponnusamy, Sangeeth Saagar
Přispěvatelé: Équipe Ingénierie Système et Intégration (LAAS-ISI), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)
Jazyk: francouzština
Rok vydání: 2016
Předmět:
Zdroj: JDF 2016-Les Journées DEVS Francophones
JDF 2016-Les Journées DEVS Francophones, Apr 2016, Cargèse, France. 9p
Popis: National audience; 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.
Databáze: OpenAIRE
Externí odkaz: