Formal Systems Development
In Formal Systems Development the scientific interests are in understanding computation in both conventional and unconventional forms, within the current computability limits or beyond, including biological and physical computational systems, together with the study of specification and development, of models and calculi for software systems and programming languages. Formal analysis, logic and algebraic computational models and theories, mechanistic and automated reasoning form a major part of this work.
The notion of development is key in computer science, and our study of development has centred on our work on refinement. Refinement can be seen as the process of moving between abstraction levels, and we seek to understand the foundations of refinement as well as its generalisations.
The engineering aspects of the field involve the application of these theoretical ideas and processes to realistic, complex problems and in the evaluation of the usability of the approaches in a realistic application environment. Techniques for the analysis of large scale problems, such as model checking, are an important part of this work. Developing novel approaches to algorithms and problems solving using approaches inspired by biological models of computation.
People:
John Derrick, Marian Gheorghe, Mike Holcombe, Siobhan North, Tony Simons, Mike Stannett, Georg Struth.
Projects:
FORSE: Formally-based tool support for Erlang development
Higher Order Refinement Techniques for the Model Driven Architecture: The key idea behind MDA is to first develop platform independent models, and then use transformations to refine to specific platforms and architectures. The platform independent models provide abstract architectural and process specifications of systems, independent of the choice implementation technologies.
Integrated specification notations: Complex computer systems are difficult to implement correctly. To aid the process formal methods use mathematics in the specification of a systems requirements and its refinement into more detailed designs and program code.
RefineNet: The UK refinement network
Refinement of State Based Systems: Investigate the theoretical and methodological aspects of refinement of state based systems, with an eye towards their usage in describing distributed systems.
Z To SAL: Complex computer systems are difficult to implement correctly. To aid the process formal methods use mathematics in the specification of a systems requirements and its refinement into more detailed designs and program code. In this project we are concerned with providing tool support for the formal specification language Z.
Hypercomputation Research Network: Hypercomputation concerns the study of computation beyond that defined by the Turing machine. It is a multi-disciplinary research area with relevance across a wide variety of fields, including computer science, philosophy, physics, electronics, biology, and artifical intelligence.
Types: The research is to develop the technology of formal reasoning and computer programming based on Type Theory.
Molecular X machines: New computational paradigms based on P systems and X machines.
Molconet: EU network of excellence on molecular computing.