Skip to main content

CS412 Formal Systems Development

Academic Aims

To study methods for designing, analysing and programming complex computing systems.

This module uses formal techniques to explore the specification, design and implementation of example computer systems. It will cover more advanced features of specification and introduce data and functional refinement, considering how a system design may be modified in a variety of practical ways. Refining the specification to code is an important step in the software life-cycle. This module presents both the theoretical basis for this and practical means of refinement from system specification to program code.

Learning Outcomes

At the end of the module the student should be able to:

  • Write formal specifications in one or more chosen notations.
  • Understand the principles of formal verification and weakest precondition and the rules for specification consistency.
  • Work with online tools to develop specifications; to generate and prove obligations for machines consistency and correctness of refinements; to refine specifications and develop code.
  • Understand the principles of refinement and the formal rules that apply. Be able to find loop variants and invariants and to verify loops.

Content

Revision of sets, relations, functions and sequences.

Revision of basic specification skills.

Introduction to development tool

  • Basic syntax
  • Introduction to the AMN approach
  • Examples and use of tool

Case studies

Data refinement

  • Refinement
  • Relations and nondeterminism
  • Simulations

Functional Refinement

Review of refinement concepts using the Guarded Command Language

Assignment

  • Logical constants
  • Sequential composition
  • Conditional statements
  • Iteration

Implementation through refinement

Throughout the module there will be an emphasis on mathematics principles, tool support and the application of techniques in domains such as computer secuity and computational modelling.

Speakers from industry on the application of formal systems development, inclduing relevant case studies.

15 CATS (7.5 ECTS)
Term 1

Organiser:
Jane Sinclair

Syllabus

Online material