A Logic with Temporal Glue for Mixed Specifications
Marc Aiguie, Fabrice Barbier, Pascal Poizat · Electronic Notes in Theoretical Computer Science · 2004
Separation of concerns or aspects is nowadays recognized as an important issue in software engineering, both at the programming and at the design/specification level. The goal of mixed specification languages (e.g. SDL, value-passing process algebras such as extensions of CSP or full-LOTOS, Korrigan) is to take into account all - or at least several - aspects of systems. We found out from our experience that a lot of mixed specification languages do share most of their features. However, specific theories, such as the symbolic transition systems one, still have to be studied for several families of mixed specification languages. In this paper we propose a logic with an expressive temporal gluing mechanism. This logic aims at providing an abstract denotational semantics for mixed specification languages. This logic enables one to reason about mixed specifications at a high level, without targeting a specific model or language. We show how our logic can be seen as an institution, which has the benefits of enabling a common refinement theory for mixed specification languages.