MONACO — A domain-specific language supporting hierarchical abstraction and verification of reactive control programs

Domain-specific languages aim to present software in the notations of domain experts and allow a straightforward mapping of application concepts to software solutions. In this paper, we present a domain-specific language for programming reactive control programs. The language differs from other approaches mainly by its hierarchical component approach, in which lower-level components provide elementary operations and upper components rely on the operations of their subordinates to implement higher control tasks. Moreover, the hierarchical component approach is leveraged in a hierarchical verification technique in which component implementations are verified against dynamic contracts of their subcomponents. We present the principles of the verification technique and discuss how it can be applied in a multi-stage development process.