Unified modeling and verification of logic controllers for physical systems

The paper describes a modeling approach that aims to provide a unified framework for the specification and verification of logic controllers for multi-domain physical systems. The proposed modeling methodology is based on the cardinal principle of object orientation, which allows to describe both control software and physical components using the same basic concepts, like classes and interface ports, and the same modeling notation, based on the UML language. Thanks to this unified approach, it is possible to describe structural and behavioral aspects of any multi-domain system coupled with a logic control device. Moreover, the behavior of the closed-loop system can be analyzed with formal verification techniques for hybrid systems, in order to prove correctness properties otherwise difficult to verify considering only discrete-event models.