Skip navigation
Please use this identifier to cite or link to this item:

Title: From non-autonomous Petri net models to executable state machines
Authors: Barros, João Paulo
Gomes, Luís
Keywords: Cyber-physical systems
Finite state machines
Formal specification
Formal verification
Petri nets
Visual languages
Nonautonomous Petri net models
Executable state machines
Readable language
Executable code
Higher-level modelling language
Verification tools
Graphical modelling language
IOPT Tools
model-driven development
Formal specification
input-output place-transition nets
Concurrent computing
Embedded systems
Issue Date: Jun-2019
Publisher: IEEE
Abstract: Petri nets have long been known as a readable and powerful graphical modelling language. In particular, Petri nets also allow the creation of high-level models of embedded controllers. These models can be translated to executable code. This possibility is already available in some tools including the IOPT Tools. Another possibility is to translate the Petri net model into a state machine, which can then be easily executed by an even larger number of platforms for cyber-physical systems. In that sense, this paper presents a tool that is able to generate a state machine from a non-autonomous class of Petri supported by the IOPT Tools framework (which is publicly available). These state machines would be too large to be manually generated, but can now be automatically created, simulated, and verified using an higher-level modelling language. The state machines can then be used for execution or even as input for additional verification tools. This paper presents the translation algorithm and an illustrative example.
Peer reviewed: yes
metadata.dc.identifier.doi: 10.1109/ISIE.2019.8781246
Publisher version:
Appears in Collections:D-ENG - Comunicações com peer review

Files in This Item:
File Description SizeFormat 
From non-autonomous Petri net models to executable state machines.pdf877.38 kBAdobe PDFView/Open

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Currículo DeGóis 

This item is licensed under a Creative Commons License Creative Commons