Encapsulating deontic and branching time specifications

  • Castro P
  • Maibaum T
  • 5

    Readers

    Mendeley users who have this article in their library.
  • 0

    Citations

    Citations of this article.

Abstract

In this paper, we investigate formal mechanisms to enable designers to decompose specifications (stated in a given logic) into several interacting components in such a way that the composition of these components preserves their encapsulation and internal non-determinism. The preservation of encapsulation (or locality) enables a modular form of reasoning over specifications, while the conservation of the internal non-determinism is important to guarantee that the branching time properties of components are not lost when the entire system is obtained. The basic ideas come from the work of Fiadeiro and Maibaum where notions from category theory are used to structure logical specifications. As the work of Fiadeiro and Maibaum is stated in a linear temporal logic, here we investigate how to extend these notions to a branching time logic, which can be used to reason about systems where non-determinism is present. To illustrate the practical applications of these ideas, we introduce deontic operators in our logic and we show that the modularization of specifications also allows designers to maintain the encapsulation of deontic prescriptions; this is in particular useful to reason about fault-tolerant systems, as we demonstrate with a small example. © 2011 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Bisimulation
  • Category theory
  • Formal methods
  • Software engineering
  • Software specification

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • Pablo F. Castro

  • Thomas S.E. Maibaum

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free