Model checking timed safety instrumented systems

ABSTRACT: Defects in safety-critical software systems can cause large eco-nomical and other losses. Often these systems are far too complex to be tested extensively. In this work a formal verification technique called model check-ing is utilized. In the technique, a mathematical model is created that cap-tures the essential behaviour of the system. The specifications of the system are stated in some formal language, usually temporal logic. The behaviour of the model can then be checked exhaustively against a given specification. This report studies the Falcon arc protection system engineered by UTU Oy, which is controlled by a single programmable logic controller (PLC). Two separate models of the arc protection system are created. Both mod-els consist of a network of timed automata. In the first model, the controller operates in discrete time steps at a specific rate. In the second model, the con-troller operates at varying frequency in continuous time. Five system spec-ifications were formulated in timed computation tree logic (TCTL). Using the model checking tool Uppaal both models were verified against all fiv