Research Projects


Title: COMPASS – Comprehensive Modelling for Advanced Systems of Systems
Start date: 2012 / End date: …
Description: COMPASS will augment existing industry tools and practice with an underlying modelling language in which Systems of Systems (SoS) architectures and contracts can be expressed. A formal semantic foundation the first to be developed specifically for SoS engineering will enable this language to support analysis of global SoS properties. The language and methods will be supported by an open, extendible tools platform with integrated prototype plug-ins for model construction, dynamic analysis by simulation and test automation, static analysis by model-checking and proof, and links to an established architectural modelling language (SysML). These strengthened foundations and tools will support enhanced methods guidelines that help users embed this new technology in industrial SoS practice. Technical advances in COMPASS are focussed on industry needs evaluated through substantial industry-led case studies in three diverse and complementary areas. These will be augmented by challenge problems solicited from a range of SoS stakeholders and developer organisations through a special interest group. The open platform, tools plug-ins, semantics, development guidelines, industry case study experience and challenge problems will ensure that COMPASS‟s outputs can be readily exploited by SoS developers and stakeholders as well as in future research and development.



Title: Refinement Calculi for Sequential and Concurrent Programs
Start date: 2001 / End date: 2002
Description: This proposal is for two Visiting Fellowships, for one month each, to enable Dr Ana Cavalcanti and Dr Augusto Sampaio of the Federal University of Pernambucco (UFPE), Brazil, to work with Prof. Jim Woodcock at the University of Oxford; and for a travel grant to enable Prof. Woodcock to visit UFPE. Drs Cavalcanti and Sampaio are experts in the field of the formal refinement of computer programs from mathematical specifications. Recent collaboration between UFPE and Oxford has resulted in the development of a refinement calculus, in the spirit of Morgan’s, specifically for Z notation. This work is now being extended and developed to allow the formal, stepwise refinement of impressive CSP programs. This concurrent refinement calculus is novel, finding its basis in the Unifying Theory of Hoare & He. The new calculus is formed from the semantic combination of Z and CSP: Z is used to give specifications in state-based and behavioural terms; operation schemas are first-class process citizens; refinement laws introduce the combinators of process algebra and the imperative mechanisms. The Principal Investigator and the proposed Visiting Fellows are currently working on a formal semantics that is sufficiently tractable to allow machine proofs of consistency and the derivation of refinement laws.


Title: Provably Correct Systems (Keep-in-Touch Activity, funded by the European Comission)
Start date: 1994 / End date: 1997
Description: UNIVERSITIES INVOLVED: Federal University of Pernambuco (Contact: Augusto Sampaio) Oxford University Computing Lab (Contact: Prof. C.A.R. Hoare ) Technical University of Denmark (Contact: Prof. Anders P. Ravn ) Carl von Ossietzky University of Oldenburg (Contact: Prof. Ernst-Rudiger Olderog ) Christian-Albrechts-University of Kiel (Contact: Prof. Hans Langmaack ) OBJECTIVES: The co-operation proposed here is in the context of the ESPRIT Basic Research PROCOS II project (no.7071) on Provably Correct Systems, dedicated to cover the entire development process for critical embedded systems, from the original capture of requirements to the computers and special purpose hardware on which the developed programs run. The emphasis is on a constructive approach to correctness, using proven algebraic transformations between adjacent phases of development: specifications, designs, programs, compilers and hardware. The purpose of this co-operation is to explore the development of embedded systems in such a way that the final implementation may include both software and hardware components. Rather than producing only machine code as the final implementation (as stated in the original objectives of PROCOS I), the aim is to design a partitioning algorithm which, based on some function of cost, determines what should be implemented in software and in hardware. The main concern is not the discovery of an original partitioning algorithm, but rather a correct design of (possibly an existing) one. RESULTS: A partitioning algorithm has been designed as a set of transformation rules which are provably correct from the semantics of the programming language. The result of the partitioning is still a program, but its structure reflects the software and hardware components, and how they interact to achieve the overall goal. We have implemented this strategy by coding the transformations in a term rewriting system.