Hybrid specification of reactive systems : an institutional approach

• Autor(es): Madeira, A. ; Faria, José Miguel ; Martins, Manuel A. ; Barbosa, L. S.
• Data: 2011
• Identificador Persistente: http://hdl.handle.net/1822/15370
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Reactive systems; Hybrid logic; Theory of institutions
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

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.