COMP8160: Practical Formal Methods in Critical Systems

(6 units)

First Semester

30 one-hour lectures and 6 two-hour Laboratory sesions

Lecturer: Dr. Malcolm Newey

Prerequisites

It will be assumed that the student has at least the mathematical maturity that is normally expected of any engineering graduate and some acquaintance with discrete mathematics, especially logic and set theory. It is essential students have experience with the process of implementing models of systems as software artifacts.

Co-requisites

There are no corequisites.

Syllabus

This course is intended to extend the general principles of model-based development to include formal system/software specification, particularly at the system/software requirements level. Students will learn how to specify systems/software using several different formal languages. They will also learn the practicality of using formal logic for demonstrating proofs of system/software behaviour.

Assessment

Assessment of a student's performance in the course will be based on marks for a final exam (50%) and marks for assignment work (50%). Some assignment work may be done in small groups.

Description

Regardless of development method, the life cycle of a software system features certain products which model the system to be created and these descriptions form a basis from which other products are derived, either mechanically or manually.

Verification of a system requires the systematic assembly of evidence that there is consistency of semantics across all products. The case must be made with a level of rigour that is appropriate to the level of risk deemed acceptable.

For critical systems, social processes (such as inspections) and natural language specifications are are a source of concern. In such cases mathematical language can be used to express system models, behaviours, properties and the transformations between life cycle products.

In this course the student will be introduced to several notations that are representative of the formal languages that are widely used for the specification of systems, for the description of transformations and for the proof of properties.

A crucial advantage of formal notations is the fact that they are mechanically manipulable, making proofs of properties completely checkable. Students in the course will get an introduction to representative tools that are used for theorem proving and model checking.

Rationale

ISO 12207 defines verification to be "the confirmation by examination and provision of objective evidence that specified requirements have been fulfilled". In the case of critical systems such objective evidence must support the conclusion with certainty. It is because of this requirement for absolute rigour that mathematical notations are used for specification and formal logic is used to derive conclusions.

Although formal (mathematical) methods will not replace testing and inspections in software engineering it already is an option that is used where the consequences of failure are extremely undesirable. As the support technology for formal methods improve we may even see them used on large non-critical software developments merely for reasons of cost-effectiveness, as is now the case in the realm of computer design.

The rationale for this course is that we believe that all software engineers should be at least aware of how formal methods are applied in critical systems, of why they may be more widespread in the future and be comfortable enough with logical notations that they can consider them as real options in software system development.

Ideas

This course will carry the main responsibility for teaching:

• a selection of suitable mathematical notations that are appropriate to specification of requirements.
• practical proof techniques relevant to the verification of system properties.
• Making students aware of a range of tools that support the use of formal methods in the software development life cycle.

The course shares with COMP8130 the responsibility for covering the subject of verification and validation.

Objectives

Upon completion of this course, the student will be able to:

• Specify systems using a schema based system such as Z;
• Use tools, such as the HOL system, to prove properties of a formally specified system;
• Specify behaviours of a concurrent system using Petri Nets;
• Use a model checker to verify properties of a system.

Topics

The following topics will be covered:

• The scope of formal methods in SE
• The family of mathematical logics
• Higher order logic
• Mechanization of logics
• System modelling
• Specification in Z
• State machines
• Petri nets
• Temporal logic
• Model checkers
• Language semantics and verification

Technical Skills

In addition to acquiring skills in the use of particular notations and techniques that form the subject matter of the course, students will also gain some experience with tools that support the use of formal methods. They will also get some practice with the functional language, ML.

Recommended Reading

• John Fitgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, 1998.
• Claude Girault and Rudiger Valk. Petri Nets for Systems Engineering. Springer-Verlag, 2002.
• Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
• Fred Kroger. The Denotational Description of Programming Languages. EATCS monographs on Theoretical Computer Science. Springer-Verlag, Berlin, New York, 1987.
• Thomas F. Melham. Higher Order Logic and Hardware Verification, volume 31 of Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1993.
• James L. Peterson. Petri Net Theory and the Modelling of Systems. Prentice Hall, 1981.
• Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall, 1996.