Towards a Theory of Interface-Based Design of Hierarchical Reactive Systems

摘要

This paper presents a formal methodology for hierarchical interface-based design of component-based reactive automation systems with behavioral contracts. Based on seminal work of de Alfaro and Henzinger, a hierarchical component approach with behavioral interface contracts and verification methods for checking that components fulfill specified contracts is presented. In contrast to other approaches, components form a strict hierarchical structure of upper and subordinate components. We discuss different questions which arise in such settings and present formal methods to answer those. Moreover, as an extension of the interface-based design methodology, a method is introduced which allows deriving the externally observable behavior of a component as a structure-preserving abstraction.