Modular deductive verification method for hybrid systems

摘要

Hybrid Systems are digital real-time Systems that are embedded in analog environments. It is important to guarantee their qualities. In order to guarantee them, we propose modular specification and verification method for hybrid systems as follows: (1) In order to represent a modular specification of hybrid systems, we developed phase transition modules. (2) In order to guarantee feasibilities of modular computations, we propose verification methods of receptiveness. (3) In order to deductively verify safety and liveness properties of each module, we developed verification rules.