Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados

Abstract

This work describes a methodology for automatic code generation for embedded systems, from a Petri net, in order to minimize the time spent in coding the program and fully automate the process of transformation. The proposed approach adopts the executable specification based on Petri Nets, where can be verified some of their properties such as deadlock, liveness, boundedness, reachability among others. Petri nets contain transitions that may have annotated codes in the C and NXC programming language, that perform specific parts of the system that is being modeled. Additionally, the annotated codes in the C programming language will be verified by a Bounded Model Checker, that it will test specific properties in the code, as a index of arrays, division by zero, safety pointers and other. This specification provides the basis for the user to display the functionality of the system that will be modeled, giving the user an overview of the specific features of the system. Thus, this methodology contributes to developers and software engineers in the generation of prototypes that represent an executable specification, facilitating the evaluation of different models and helping to reduce differences of interpretation in the construction of software. This work also presents a tool called PNTCG (Petri Net Tool for Code Generation) developed based on this methodology and a case study based on a prototype automation product packaging, which uses a conveyor belt and a robot arm to demonstrate the use and application of this methodology.