Model-checking framework for embedded systems controllers development using IOPT Petri nets

This paper presents a new model-checking framework for embedded systems controllers development using IOPT Petri nets. The new tools, comprehending a state-space generator, a query system and a new automatic code generator, were added to an existing tool framework which already had tools to import and edit controller models, automatic code generators and automatic hardware synthesis tools. The new tools permit the automatic analysis of system properties and the fast detection of errors during early design stages, considerably reducing debug and validation time. All tools share the same Web based user interface, publicly available on the research group Web page (http://gres.uninova.pt).