On the automatic generation of timed automata models from ISA 5.2 diagrams
Luiz Paulo de Assis Barbosa, Kyller Gorgônio, Antonio M. N. Lima, Ângelo Perkusich, Leandro Dias da Silva · 2007
Safety Instrumented Systems (SIS) are usually designed to prevent accidents, avoid undesirable situations and guarantee continuous operation of oil and gas production systems. An interruption in the operation can be caused by faults in sensors and/or actuators. Hence, SIS are usu ally integrated to the supervisory control system in order to use the information from sensors to prevent such unde sirable situations. In this scenario, it is important to be able to validate the SIS implementation against its spec ification in order to increase the reliability of the system. In this work a technique to improve the dependability of SIS is introduced. A method to obtain a timed automata from a ISA 5.2 specification is presented and applied to a case study provided by Petrobras (Brazilian oil company). Finally, an approach to perform automatic testing of the implementation using the generated model is discussed. The method introduced here is based on the use of the Up paal model checker and the Uppaal-TRON testing tool.