Tool support to derive specifications for conflict-free composition

Tun, Thein Than; Laney, Robin; Jackson, Michael and Nuseibeh, Bashar (2008). Tool support to derive specifications for conflict-free composition. Technical Report 2008/13; Department of Computing, The Open University.

DOI: https://doi.org/10.21954/ou.ro.0001607d

Abstract

Finding specification of pervasive systems is difficult because it requires making certain environmental assumptions explicit at design-time, and describing the software in a way that facilitates runtime composition. This paper describes how a systematic refinement of specifications from descriptions of the system's environment and requirements can be automated. Our notion of requirements allows individual features in the system to be inconsistent with each other. Resolution of conflicts at design-time is often over-restrictive because it uses the strongest possible conditions for conjunctions and rules out many possible interactions between features. In order to support runtime resolution, our tool examines specifications for potential conflicts and augments them with information to enable detection at runtime. We use a form of temporal logic, the Event Calculus, as our formalism , and characterize the refinement of requirements as a kind of abductive planning. This allows us to use an existing Event Calculus planning tool, implemented in Prolog, as a basis to develop a reasoning tool for obtaining specifications from potentially inconsistent requirements. We validate our tool by applying it to find specifications of smart home software .