%0 Conference Proceedings
%T A State-Space Based Model-Checking Framework for Embedded System Controllers Specified Using IOPT Petri Nets
%+ Universidade Nova de Lisboa = NOVA University Lisbon (NOVA)
%+ ISEL
%A Pereira, Fernando
%A Moutinho, Filipe
%A Gomes, Luís
%Z Part 6: Petri Nets
%< avec comité de lecture
%( IFIP Advances in Information and Communication Technology
%B 3rd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS)
%C Costa de Caparica, Portugal
%Y Luis M. Camarinha-Matos
%Y Ehsan Shahamatnia
%Y Gonçalo Nunes
%I Springer
%3 Technological Innovation for Value Creation
%V AICT-372
%P 123-132
%8 2012-02-27
%D 2012
%R 10.1007/978-3-642-28255-3_14
%K Embedded Systems
%K Mmodel-Checking
%K Petri Nets
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 5
%Z WG 5.5
%2 https://inria.hal.science/hal-01365577/document
%2 https://inria.hal.science/hal-01365577/file/978-3-642-28255-3_14_Chapter.pdf
%L hal-01365577
%U https://inria.hal.science/hal-01365577
%~ IFIP
%~ IFIP-AICT
%~ IFIP-TC
%~ IFIP-TC5
%~ IFIP-WG
%~ IFIP-WG5-5
%~ IFIP-DOCEIS
%~ IFIP-AICT-372