Formal Verification of Hybrid Models for Physical Systems

Industrial automation is an application field in which logic controllers play a dominant role. These controllers typically interact with an heterogeneous physical system, composed by mechanical parts, electrical drives, chemical processes and so on, which means that the overall system's behavior should be represented and analyzed with tools derived from hybrid systems theory. This paper proposes a modeling approach that aims to provide a unified framework, based on the cardinal principles of object orientation, for the specification and verification of logic controllers for multi-domain physical systems. The proposed modeling methodology allows to describe both control software and physical components using the same basic concepts and the same modeling notation, based on the UML language. Moreover, the paper describes how to analyze the behavior of the closed-loop system with formal verification techniques for hybrid systems, in order to prove the correctness of the designed logic controller.