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

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 Citations (Scopus)


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.
Original languageUnknown
Title of host publicationIFIP Advances in Information and Communication Technology
Publication statusPublished - 1 Jan 2012
Event3rd IFIP/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems -
Duration: 1 Jan 2012 → …


Conference3rd IFIP/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems
Period1/01/12 → …

Cite this