A State-Space Based Model-Checking Framework for Embedded System Controllers Specified Using IOPT Petri Nets

Abstract : This paper presents a state-space based model-checking framework to test and validate embedded system controllers specified using the IOPT Petri net formalism. The framework is composed of an automatic software code generator, a state-space generator and a query engine, used to define queries applied to the resulting state-space graphs. During state-space generation, the tools collect information required to enable the efficient implementation of hardware/software controllers, including place bounds, deadlocks and conflicts between concurrent transitions. User defined queries can check relevant system properties, as the occurrence of undesired error situations, the reachability of desired states, system liveliness and the occurrence of deadlocks and livelocks. The new tool, available online under a Web based user interface, provides a fast and efficient way to test and validate system controllers, contributing to the reduction of development time.
Type de document :
Communication dans un congrès
Luis M. Camarinha-Matos; Ehsan Shahamatnia; Gonçalo Nunes. 3rd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2012, Costa de Caparica, Portugal. Springer, IFIP Advances in Information and Communication Technology, AICT-372, pp.123-132, 2012, Technological Innovation for Value Creation. 〈10.1007/978-3-642-28255-3_14〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01365577
Contributeur : Hal Ifip <>
Soumis le : mardi 13 septembre 2016 - 15:21:20
Dernière modification le : mardi 13 septembre 2016 - 17:06:05
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 13:52:25

Fichier

978-3-642-28255-3_14_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Fernando Pereira, Filipe Moutinho, Luís Gomes. A State-Space Based Model-Checking Framework for Embedded System Controllers Specified Using IOPT Petri Nets. Luis M. Camarinha-Matos; Ehsan Shahamatnia; Gonçalo Nunes. 3rd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2012, Costa de Caparica, Portugal. Springer, IFIP Advances in Information and Communication Technology, AICT-372, pp.123-132, 2012, Technological Innovation for Value Creation. 〈10.1007/978-3-642-28255-3_14〉. 〈hal-01365577〉

Partager

Métriques

Consultations de la notice

70

Téléchargements de fichiers

41