CS389

Formal Software Development

Spring Semester 2008


Course Organisation/Dates

Course Aims

Lectures

Labs

Coursework

Exams

Resource Materials


Aims

Successful large-scale formal development of software relies on approaches which have effective tool support. The object-based B-Method is currently the most complete formal development method which supports all stages of the software lifecycle from specification through design through to automatic code generation, providing a unified approach to specification, design and programming. It is particularly used in sectors of industry where safety is a concern---for example, it was recently used in the development of the control software for the automatic driverless trains on the new Meteor line of the Paris metro, and the subsequent testing of the system revealed no bugs in over 80,000 lines of code!

Learning Outcomes

This module concentrates on a verifiable approach to software development. Students who successfully complete this course should be able to:
  • develop formally correct programs
  • demonstrate full knowledge of the advanced constructs within the B-Method,
  • apply the concepts of weakest precondition to program verification,
  • carry out a refinement and verify that an implementation meets its specification,
  • analyse loops within programs and identify appropriate loop invariants and variants,
  • have experience of large case studies using the B-Method,
  • be able to describe when and how to apply design patterns in large examples,
  • have an awareness of how B code integrates with C.

Go to the University of Surrey's Home Page Hosted by Computing @ Surrey This page is maintained by Helen Treharne.