Theme leader: Antonio Cau

Theme members: Ben Moszkowski, Francois Siewe, Helge Janicke, David Smallwood, Giampaolo Bella, Hussein Zedan

Projects:

Compositional Methods for     Hardware/Software Co-Design.	EPSRC
A Compositional Approach to the Specification     of Systems using ITL and Tempura.	EPSRC

Abstract

Under this theme, we work on the theoretical foundations that underpin all our other research themes:

• Requirement and Knowledge Engineering,
• Software Evolution,
• Semantic Web and Service-oriented Computing and
• Computer Security and Trust.

Specifically we are looking at the specification and verification of critical systems in a compositional way.

Compositionality

A major strand of our research is based on compositionality, i.e., to proof a property of a system one proceeds by proving properties for all the components of the system and use these to infer that the system satisfies the overall property.

Refinement/Transformation Theory

The idea is that one starts with a high level abstract specification and use sound refinement rules to incrementally develop a low level concrete system.

• We have developed a compositional refinement theory based on Interval Temporal Logic (ITL) which is a linear time discrete temporal logic with a chop operator.
• The Fermat program transformation theory uses formal proven transformations, which preserve or refine the semantics of a program while changing its form. The core of Fermat is the WSL language which is based on infinitary first order logic. It contains all the operations needed for a programming and specification language.

Verification

We use logic based methods to verify the correctness of our systems. The logic we use is Interval Temporal Logic (ITL). We use the following types of verification tools

• Pen and paper. We have developed a compositional verification framework for ITL using the assumption/commitment paradigm. Furthermore we have a complete axiom and proof system for ITL.
• PVS: An ITL library has been developed that encodes the ITL axiom and proof system within the Prototype Verification System (PVS).
• Prover9: Prover9 is a resolution/paramodulation automated theorem prover for first-order and equational logic developed by William McCune. We have given an algebraic axiom system for Propositional Interval Temporal Logic (PITL): Interval Temporal Algebra. The axiom system is a combination of a variant of Kleene algebra and Omega algebra plus axioms for linearity and confluence. This algebraic axiom system for PITL has been encoded in Prover9. So we can use Prover9 to prove the validity of PITL theorems.
• AnaTempura: a tool for the runtime verification of systems using Tempura, an executable subset of ITL.
• FLCHECK: We have developed a decision-procedure for Fusion Logic (FL), a logic as expressive as PITL. The tool is capable of checking the satifiability and validity of FL theorems.