The Department Home Prospective Students Staff List Research Information Conferences and Workshops Industrial Liaison Departmental Vacancies Alumni Contact Us Other Links

Computing Science Current Student Information Computing Science Seminars

Maths and Stats Group M&SG Home Page Mathematics Seminars Statistical Service

The University University Home Page Student/Staff Portal WebCT

Applied Formal Methods

The Applied Formal Methods research group concentrates mainly on the application of formal methods to systems engineering and the systems development process, with some work on fundamental theory. In addition to object oriented software development, application areas include communications and distributed systems, complex systems, and biological and medical systems. The emphasis is on practical techniques and tools. Particular techniques employed include LOTOS-based design and verification, and the Omnibus development environment.

Staff

• Robert G Clark
• Tim Denvir (honorary professor)
• Simon B Jones
• Savitri Maharaj
• Charles M I Rattray (honorary reader)
• Carron E Shankland
• Kenneth J Turner

Research Students

• Chris McCaig
• Thomas Wilson

Current and Recent Visitors

The group hosted Don Batory and Michel Bidoit as part of the AMAST 2004 programme.

Research Activities

Biological Systems are proving amenable to formal description and analysis. Process algebras are suitable for describing disease systems at an individual level. Work is underway to automatically extract mean field difference equations from such descriptions to further enhance our understanding of epidemiology. This is cross-disciplinary collaborative work undertaken within the department. A further biological strand is in developing logical descriptions of cellular pathways. This is joint work with Computer Science (Arizona) and BioInformatics (Glasgow).

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. The FireWire bus (IEEE 1394) has been studied using two different techniques: E-LOTOS (Enhanced LOTOS) and μ-CRL.

CRESS 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. CRESS is graphical in order to improve 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.

CONFORMED The goal of CONFORMED (Conformance Of Radiological/Medical Devices) is to define a method for specifying, analysing and testing the functional characteristics of radiotherapy equipment used in oncology centres for cancer treatment. The specification language is LOTOS (Language Of Temporal Ordering Specification). The project has studied the characteristics of radiotherapy machines, allowing them to be modelled formally and rigorous tests to be derived for evaluating their correct behaviour.

Complex Systems need a firm theoretical base on which to develop new practical approaches. New ways of thinking about design and the design process are being developed based on category theory, the theory of shape, and the notion of approximation.

LOTOS continues to provide inspiration for a variety of new applications and theory. The LOTOS sub-group at Stirling is probably the largest working in the UK on this internationally recognised language, and has in the past been involved in developing the new ISO standard for E-LOTOS. Ongoing research provides a new theoretical framework in which to reason about process algebras with multiway synchronisation (of which LOTOS is an example). The LOTOS sub-group has developed applications in a number of new areas including bus protocols, 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 new project, underway here at Stirling, aiming to support the development of reliable software. It is built around the new 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 from run-time checking and extended static checking of lightweight assertion annotations to full formal verification with respect to heavyweight specifications.