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.
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.
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
- Relations and nondeterminism
Review of refinement concepts using the Guarded Command Language
- Logical constants
- Sequential composition
- Conditional statements
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.