COMP9116 System
Development Using Event-B:
System Modelling and Design COMP9116 System Development Using Event-B: System Modelling and Design June 29, 2014 News Outline Lectures Tutorials Assignments Event-B Rodin COMP9116: System Development Using the Event-B Lecturer Room e-mail phone Ken Robinson kenr 9385 4045 Lecturer-in-charge Lecture time Friday 1400–1700 ASB 207 (E15-1049) What’s this course about? In simple terms this course is concerned with building a model of a system based directly on the requirements. The objective is to ensure that the implementation of the model will satisfy the requirements without testing. You are unlikely to have experienced anything like this in other CSE courses. The model is not restricted to software and the implementation of the model may contain non-software components. Success is achieved by the consequent ability of being able to reason about and verify the behaviour of the model against the requirements. This is better than and completely the reverse of most software development where a software system is built and then tested to determine whether the system is consistent with the requirements. By better’ we mean better able to reasoned about, better able to make quantitative assertions. This is achieved by building a model of the required system and using mathematics to verify the consistency of the model, in much the same way as mathematics is used in other engineering disciplines. The main difference is that we use discrete mathematics, whereas other engineering disciplines, based on the physical sciences, use continuous mathematics. Our form of reasoning will use assertions, logic and theorem proving. Course Delivery This course has a small class and advantage will be taken of that to conduct the meetings each week more like tutorial sessions. The course will also have a mix of students, some of whom are familiar with EventB and others with no experience; some are undergraduate students and others are postgraduate students. Those with no experience will be encouraged to “catch up” by doing exercises from the COMP2111 course and the course will be organised with the intention of not disadvantaging either the experienced or inexperienced students. The course will be delivered using a mixture of lecture presentations and developments running on the Rodin Event-B toolkit. Event-B is the most recent development of the B Method. The earlier version of B is generally referred to as Classical B. The following topics will be covered: Overview: An overview of Event-B with some reference to Classical B and. An understanding of the differences. Using the Rodin toolkit: an overview of the Rodin toolkit, which will be used extensively in class. [Context:] contexts define constants, abstract sets, axioms and theorems providing the context for machines that contain the actions of a system. [Machines:] machines see contexts and contain variables, invariants and events. The variables and invariants describe the state and events describe the actions that can occur in the machine. [Invariants:] predicates that describe the “safety” conditions of the state of a machine. [events:] guarded autonomous actions that produce machine transitions. [guards:] predicates that describe the conditions under which an event may fire. Guards are functions of machine variables and event parameters. [Events vs Operations: ] the difference between Classical B and Event-B. How that difference affects development. [Specification: ] an abstract description of required behaviour. [Refinement: ] the process of developing a design from an abstract specification. [Implementation: ] a refinement that can be simply translated to a program that can be executed on a computer. [Animation: ] the role of animation in validating a specification. [Proof obligation generation: ] formal expresion of requirements for machine consistency and refinement satisfaction. [Proof obligation discharge: ] formal proof of proof obligations. [Machine structoring and visibility: ] machine decomposition. [Documents: ] formal document produced from Rodin. Case studies will be used to illustrate the above. Assessment The final subject grade will be computed from the assignment and the examination each weighted equally. Assignment There will be an assignment —or set of assignments— in which each student will undertake an event-B development of some small system. The assignment requirement will be developed during the lectures. Examination There will be a 3-hour examination conducted in a computing laboratory using the Rodin Toolkit. Rodin: the Event B Toolkit An event-B toolkit has been developed by a European project named Rodin. The toolkit is open-source and extensible based on the Eclipse system. The toolkit should run on any platform that has an installation of Java. The toolkit can be downloaded from http://sourceforge.net/projects/rodin-b-sharp/. http://www.event-b.org/ contains information and links for Event-B and Rodin. Textbook System Modelling & Design is a textbook being written by Ken Robinson. The book is almost finished and students will be given access to the current version of the book. Jean-Raymond Abrial’s book. See below. The course will be backed up by substantial notes, including cases studies developed by Jean-Raymond Abrial. Many documents can be found at http://rodin.cs.ncl.ac.uk/. Look, particularly, at the Deliverables page. Many case studies in Classical B will be found on the course website, and the following bibliography contains references on Classical B.
