The Applied Formal Methods research group is focussed on developing and applying a range of formally based techniques for description and analysis of complex systems. The systems under study come from a very broad variety of application domains, including object oriented software development, communications and distributed systems, biological and medical systems, and social and economic systems. The underpinning theme is the use of Computing Science techniques to model, analyse and understand these systems. Particular techniques employed include process algebras such as PEPA, Bio-PEPA and LOTOS; (quantitative) verification tools such as the PRISM model checker; simulation packages such as NetLogo; and the Omnibus software development environment. The emphasis is on practical techniques and tools, with some work on fundamental theory.
The group hosted Luigi Logrippo, University of Quebec at Gatineau (Canada) to collaborate on use of Alloy to model and analyse policies for call control.
Formal methods are proving to be useful ways of describing Biological Systems, providing insights through powerful abstraction and analysis tools. The group uses process algebras to describe disease systems at an individual level, and immunological systems at a cellular level. The important break-through of our work is the development of an automatic method to extract population level system dynamics from individual-based models. This is a cross-disciplinary collaboration mainly with the Mathematical Biology research group at Stirling, but also Biological Sciences at Liverpool, funded by EPSRC. Further biological strands regard developing simulations of disease systems using NetLogo to better understand the social and economic impacts of disease. This is also cross-disciplinary work between Computing Science and Mathematics. Also, models of the immune response to infectious diseases such has HIV are being developed under a collaboration with the University of Cambridge. Past work has focussed on describing the functioning of the calyx of Held, a synapse in the auditory tract of mammals.
Communications and Distributed Systems have been a fruitful area for the application of formal methods. Standardised formal methods, LOTOS (Language Of Temporal Ordering Specification, ISO 8807) and SDL(Specification and Description Language, ITU-T Z.100) are mainly used as they are of most interest to industry and have good tool support. Research has been undertaken on methods of structuring communications services. This generates their formal representation in an architecturally sound manner. There is some cross-fertilisation with the Communications and Services Group, particularly in the area of analysis of multicast protocols.
CRESS (Chisel Representation Employing Systematic Specification) is a notation and set of tools for graphical specification and analysis of services. CRESS has specialised support for combining services in a graphical way that improves its attractiveness to an industrial audience. Automated tool support has been developed to check the correctness of diagrams and to translate them into various formal languages and implementation languages. The toolset is portable and can run on a variety of platforms with a variety of front-end diagram editors and back-end target languages. Most recently, CRESS has been further developed for application in the web and grid services domain.
The ISO standard LOTOS continues to be a subject of active use. The LOTOS sub-group at Stirling has been the largest working in the UK on this internationally recognised language. Stirling staff were also involved in developing the new ISO standard for E-LOTOS. Foundational work has included development of a new theoretical framework in which to reason about process algebras with multi-way synchronisation (of which LOTOS is an example). The LOTOS sub-group has developed applications in a number of new areas including bus protocols, decision support, hardware description, medical devices, object-oriented analysis and design, Quality of Service, and telecommunications services. The Department maintains the LOTOS world-wide web pages called WELL (World-wide Environment for Learning LOTOS) for the international community.
Omnibus is a development environment supporting reliable software. It is built around the Omnibus language which is designed to be both amenable to formal analysis and familiar to Java programmers. The language is supported by an integrated development environment providing a range of assertion-based verification tools including run-time checking, extended static checking of lightweight assertion annotations, and full formal verification of heavyweight specifications. Omnibus is no longer under current development.
Process algebra are also being used for applications to crowd dynamics with the aim of developing computationally inspired models of the emerging behaviour of a multitude of related individuals who are displaced in a given (physical) environment, such as a crowd during an emergency egress. Being able to (formally) reason about these models will allow us to tackle specific issues, such as how an emergency egress is affected by a hurt evacuee obstructing a passage or by the choice of the width of the doors in the building or by the evacuation strategy adopted, and address crowd behaviour in potentially critical and risky situations in general. This research is carried out in collaboration with the University of Edinburgh and the ISTI-CNR in Pisa.