Theory and Computational Paradigms
Theme leader: Antonio Cau
Theme members:
Ben Moszkowski,
Francois Siewe,
Helge Janicke,
David Smallwood,
Giampaolo Bella
Projects:
Abstract
Under this theme, we work on the theoretical foundations that
underpin all our other research themes:
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 firstorder 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 decisionprocedure for
Fusion Logic (FL), a logic as expressive as PITL.
The tool is capable of checking the satifiability and validity of FL
theorems.
