Current postgraduate taught students
COMP60110: System Construction Using B (2007-2008)
It has been known for a long time that in theory, the whole activity of system specification, refinement and implementation, could be integrated into a comprehensive mathematical theory and could be supported by industrial strength system development tools. However actual realisations of this supposition were slow to appear. The B-Method was the first to do so, and the method is particularly suited to the building of the kind of state machines found at the heart of many safety critical software control systems, such as train safety systems. (The B-Method has achieved world-wide acclaim in the construction of many underground and local rail systems.) Central to the success of the B-Method is the use of tools, such as the B-Toolkit and Atelier-B. These allow the mechanisation and automated checking of the whole development process. The aim of the course is to give a solid grounding in the B method, using Event-B (a recently created variant of the B-Method), and supported by the Rodin tool (an equally recently created new toolkit for mechanically underpinning Event-B), enabling students to go on to participate in the rigorous building of real systems.
This course unit aims to:
introduce the formal methods landscape and the place of Event-B in it,
introduce the basics of Event-B,
develop familiarity with Rodin,
develop proficiency in Event-B via case studies and practical sessions,
give exposure to interactive proof in Rodin,
provide group mini-projects to develop particular application areas using Event-B and Rodin.
A student successfully completing this course unit should:
have an understanding of the role of formal software development and its advantages and disadvantages (A),
have an understanding and knowledge of the essential elements of Event-B (A,B,C),
be able to develop small applications using Event-B and Rodin (B,C),
be able to undertake the investigation of a larger application using Event-B and Rodin (B,C,D),
be able to prepare a technical report on a study performed using Event-B and Rodin (C,D),
be able to work effectively as a member of a group to undertake a mini-project using Event-B and Rodin (D).
Assessment of learning outcomes
Learning outcomes (1), (2) and (3) are assessed by examination (closed book), learning outcomes (3), (4) and (5) are assessed by laboratory reports, learning outcome (6) is assessed by mini-project.
Contribution to programme learning
A1, A2, B2, B3, C1, C2, C4, D1, D3, D4.
Special resources needed to complete the course unit
Rodin is freely available and you can install it on your own machine if you wish. See the Rodin Sourceforge site. The Windows and Mac binaries are reliable. The Linux binary was developed under Ubuntu and is reputedly reliable under Suse, but (currently) cannot be depended on under Fedora.
Assessment of Learning outcomesA student successfully completing this course unit should:
1. have an understanding of the role of formal software development and its advantages and disadvantages (A),
2. have an understanding and knowledge of the essential elements of Event-B (A,B,C),
3. be able to develop small applications using Event-B and Rodin (B,C),
4. be able to undertake the investigation of a larger application using Event-B and Rodin (B,C,D),
5. be able to prepare a technical report on a study performed using Event-B and Rodin (C,D),
6. be able to work effectively as a member of a group to undertake a mini-project using Event-B and Rodin (D).
Week 1: Introduction to Formal Methods in System Design. Introduction to the Event-B Methodology. Case study: Cars on a Bridge. Practical Work: Getting Started with Rodin and Exercises 1.
Week 2: Review of Exercises 1. Case study: Developing a File Transfer Protocol. Mechanical Proof. Practical Work: Exercise 2.
Week 3: Case studies: Leader Election, Synchronising Processes. Developing Sequential Programs. Practical Work: Exercise 3.
Week 4: Case study: A Mechanical Press Controller. Project Allocation. Practical Work: Exercise 4.
Week 5 to end of course: Project Work.