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

Filipe Moutinho; Luís Filipe dos Santos Gomes

doi:10.1007/978-3-642-28255-3_14

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

Filipe Moutinho, Luís Filipe dos Santos Gomes

DEE - Departamento de Engenharia Electrotécnica e de Computadores

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Citations (Scopus)

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.

Original language	Unknown
Title of host publication	IFIP Advances in Information and Communication Technology
Pages	123-132
Volume	372
DOIs	https://doi.org/10.1007/978-3-642-28255-3_14
Publication status	Published - 1 Jan 2012
Event	3rd IFIP/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems - Duration: 1 Jan 2012 → …

Conference

Conference	3rd IFIP/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems
Period	1/01/12 → …

Access to Document

10.1007/978-3-642-28255-3_14

http://oa.uninova.pt/5083/

Cite this

@inproceedings{63a39ef307274afcaacf47a12ed8989c,

title = "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.",

keywords = "Model-Checking, Embedded Systems, Petri Nets",

author = "Filipe Moutinho and Gomes, {Lu{\'i}s Filipe dos Santos}",

note = "Sem PDF; null ; Conference date: 01-01-2012",

year = "2012",

month = jan,

day = "1",

doi = "10.1007/978-3-642-28255-3_14",

language = "Unknown",

isbn = "978-3-642-28255-3",

volume = "372",

pages = "123--132",

booktitle = "IFIP Advances in Information and Communication Technology",

}

TY - GEN

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

AU - Moutinho, Filipe

AU - Gomes, Luís Filipe dos Santos

N1 - Sem PDF

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

KW - Model-Checking

KW - Embedded Systems

KW - Petri Nets

U2 - 10.1007/978-3-642-28255-3_14

DO - 10.1007/978-3-642-28255-3_14

M3 - Conference contribution

SN - 978-3-642-28255-3

VL - 372

SP - 123

EP - 132

BT - IFIP Advances in Information and Communication Technology

Y2 - 1 January 2012

ER -