Automatic Verification of Critical Industrial Process with Automata

• Luis E. Mendoza Morales Universidad Simón Bolívar-Venezuela

Abstract

A goal of the designers of business and system developers is to build reliable software applications, providing the systems to automate the processes that constitute the objective of an industry, known as Critical Industrial Processes (CIP). One way to achieve this goal is using formal verification techniques such as Model Checking (MC), which increases understanding of automated processes, revealing inconsistencies, ambiguities and incompleteness, which are not easily noticed. This paper presents the integration of a Formal Compositional Verification Approach with the timed automata theory for the specification, and the MC of the Tasks Model (TM) associated with a CIP (IPTM). The result is a methodological infrastructure that guarantees the accuracy of IPTM respect to the specification of the initial properties derived from good practices and industrial standards. Through a typical example to evaluate methodologies for designing automated industrial systems, the integration of the MC in the early stages of CIP design is shown.