University Of Pretoria SA Coronavirus Website Computer Science Department

COS740 - Formal Methods (1)


Module Content

Practical - Task Specification Booklets
The first practical! (The submission deadline date will be announced separately, after we have obtained more clarity about the currently ongoing COVID19 quarantine time...)
The second practical! (The submission deadline date will be announced separately, after we have obtained more clarity about the currently ongoing COVID19 quarantine time...)
Mark Sheet - Your current status of the semester marks...
Status Date: 28th of May, 2020
Background: Event-B and Rodin - Background: Please look into these materials in addition to our textbook.
by Hugo Gimbert.
by Thai Son Hoang.
by C. Métayer, J.-R. Abrial, and L. Voisin.
by Michael Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, and Laurent Voisin.
Final exam: Task specification. Work-time: 6-8 July 2020.

Module forums

The new CS forums are available here.

Module Links

>>What is the relationship between Rodin proof obligations (POs) and ProB. In short, ProB can be made to check individual proof obligations...<< [by Michael Leuschel]
>>Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof...<<
The tool Pro-B.
More about Event-B and Pro-B.
BACKGROUND Reading: Slide-Show from the University of Vienna (Austria) on the difficulties of modelling, on the CENELEC standard, etc...


Remember Me

Module Description

THIS WEB PAGE IS THE STUDY GUIDE for COS740: FORMAL METHODS. Please carefully take note of all further announcements which will appear on this web page....

Show Long Description

Lecturer Information

Course Coordinator

Prof Stefan Gruner


Assistant Lecturers


There are no tutors assigned.

Teaching Assistants

There are no teaching assistants assigned.

Class Representatives

Active Assignments

No currently active Assignments.
Check the assignment portal:

Active Fitch Fork Assignments

No currently active Fitch Fork Assignments
Check the assignment portal:

Active Bookings

    No bookings available

Lab Bookings

    No lab bookings available

Active Team Allocations

    No team allocations available

Active Bids

Individual Bids

    No individual bids

Team Bids

    No team bids

Team Pages

Team Pages

    No Team Pages

Team Pages Open to Module Members

    No Public Team Pages

Team Pages Open to Everyone

    No Public Team Pages

Active Polls

How is it going with home-studying during COVID19?

I am still coping = in good spirits
I am struggling = it is difficult
Feeling overwhelmed = cannot cope any more

Progress with Practicals

I have not yet completed any practical
I have completed P1, however not yet P2
I have completed P2, however not yet P1
I have already completed both practicals

All content copyright © Department of Computer Science, School of IT, University of Pretoria, South Africa