Modelagem, verificação formal e codificação de sistemas reativos autônomos

Abstract

The computation systems are used in many areas, since bank account´s until patient's monitoring. Applications where human lives and high investments are critical, the system´s quality is fundamental to reduces or eliminate failures. The formal methods are used to describe parts of the system using appropriate level of abstraction. This thesis presents the Bare Model to development of applications in Autonomous Reactive System´s and shows his capabilities to development many applications. The model starts with a application description by a finite state machine, called X-machine. The application acts as a centerpiece, or core, of a reactive system. The events detected in the environment are captured and evaluated, based on the current state of the machine. The response to the events detected are the transitions of states and the actions, which can be an new event or just a communication. On the Bare Model, the specification of the application is done by using a graphical tool called GeradorXM. After the design, the X-machine is transformed to a tabular model, where each line is independent and contains enough information to perform a computation. The tabular model is uploaded into the target hardware, where it is interpreted by a small code, called ExecutorXM, which is responsible for his execution. Before to run the application, a model of the system can be generated to be used as an input to the NuSMV, which is a model checking's tool. Thus the desirable properties for the application may be checked to confirm its correctness. Thus closing a cycle of applications development to autonomou´s reactive systems using a formal model, with automatic code generation which is executed by an translator and using formal verification of properties for the system model.