Hybrid specification of reactive systems : an institutional approach

• Author(s): Madeira, A. ; Faria, José Miguel ; Martins, Manuel A. ; Barbosa, L. S.
• Date: 2011
• Persistent ID: http://hdl.handle.net/1822/15370
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Reactive systems; Hybrid logic; Theory of institutions
• Document Type: Article
• Language: English

Description

This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper’s main contribution is to pro- vide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them.