HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Tuesday, September 13, 2016 - 3:21:20 PM
Last modification on : Tuesday, June 29, 2021 - 12:20:08 PM
Long-term archiving on: : Wednesday, December 14, 2016 - 1:52:25 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Fernando Pereira, Filipe Moutinho, Luís Gomes. A State-Space Based Model-Checking Framework for Embedded System Controllers Specified Using IOPT Petri Nets. 3rd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2012, Costa de Caparica, Portugal. pp.123-132, ⟨10.1007/978-3-642-28255-3_14⟩. ⟨hal-01365577⟩



Record views


Files downloads