Resources

MUSO | Books | Lecture Slides | Event-B Resources | Web Documents

MUSO

The faculty is trialling the use of Moodle as a MUSO subsystem, and FIT3013 will be run using Moodle as the primary contact point for the unit. The courseware for the unit has been developed using XML, which cannot be employed directly within Moodle, but is accessible through the Moodle pages. This should be largely transparent when navigating within Moodle, but be aware that all the courseware is available without logging on through Moodle at http://www.csse.monash.edu.au/~ajh/teaching/fit3013/2010/. This server runs a python script to convert the XML pages to HTML on the fly, and thus renders them as pages visible under Moodle.

This actually has the advantage that you can navigate between pages using the MUSO navigation, or using the FIT3013 page navigation. Your choice!

Note that the Grade Book in Moodle is not duplicated within these pages, but is accessible (with login to Moodle).

If you do have any problems with MUSO (such as missing assignments!), then please see the faculty MUSO person, Margot Schuhmacher, who is in room 125, building 63, Clayton campus, Monday to Thursday (ext 58313).

Books

The prescribed text book is:

Schneider, Steve
the b-method
palgrave

Unfortunately, there is no text book that describes Event-B directly. The Schneider text describes the B-Method, upon which the Event-B method is based. There are also manuals available through the Moodle and resources pages.

Lecture Slides

The lectures are derived from slides kindly provided by Professor Ken Robinson of the University of New South Wales, modified for local use. The lecture slides are on-line. See the timetables page for detail of the sequencing of these slides.

Event-B Resources

There is a very convenient Event-B Summary page prepared by Prof Ken Robinson. There is also a smaller version, suitable for double sided printing as a reference card. Printed copies of this are available from the lecturer.

There is a set of notes on the B Method (the precursor to Event-B) available here

Rodin

The practical work is based upon the Rodin tool suite, which is available for download from the Event-B website. This site also contains documentation of the Rodin Platform. Versions for Windows, Linux, and Mac OS X are available from this subpage.

Adding LaTeX to Rodin

You need first to install the B2LaTeX plug-in. Go to the menu item Help -> Software Updates ... and select B2LaTeX in the window that appears. Follow the install prompts. A restart is encouraged, once the plug-in is installed.

You should now see a little Lx icon in the menu bar. Clicking this icon in the Edit or Pretty Print windows will write a LaTeX file into your workspace.

Processing this LaTeX file is a little tricky. You need to find your workspace - if you don't know where you set it on installation, the easiest way to find it is to open Rodin -> Preferences -> General -> Startup and Shutdown, and tick the box "Prompt for workspace on startup". Restart Rodin, and a dialog box will appear with the workspace name. Make a note of this directory!

Within it you will find a subdirectory for each project. Inside the project directory for the project you clicked the Lx icon, you will find a "latex" subdirectory. In this will be one or maore LaTeX files which you can process with LaTeX to get a pdf file of your project specification. Note that it needs the two style files b2latex.sty and bsymb.sty. For some reason, b2latex.sty is supplied, but not bsymb.sty. You can download it from here or from the Event-B website.

Of course, you will need a working copy of LaTeX! Download it from here if you haven't already.

Sample Machines

Some of these machines are described in lectures.

Date	Machine
20100304	The Parking Meter Machine
20090316	The Bridge Context, refinement 0 The Bridge Machine, refinement 0
20090330	The Simple Library Context The Simple Library Machine

External Web Pages

A paper that describes the design process used for the platform screen doors of the Paris RATP train system is available at http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf

Web Documents

Date Published	Number	Document Name
20091216	00	Home Page
20100121	01	Web Documents
20100121	02	Timetables
20100210	03a	Assignment 1
20100218	04	Assignment 1 index page
20100224	05	Learning Modules
20100224	06	Unit Timetable
20100224	07	Lectures
20100224	08	Learning Module 1: Introduction
20100224	09	Assessment
20100301	10	Unit Resources
20100301	10	Learning Module 2: Review of Set Theory
20100301	12	Teaching and learning Methods
20100301	13	Tutorials
20100303	14	Discussion
20100303	15	Discussion Topic 1
20100304	16	Tutorial 1

20090203	08	Learning Module 3: Abstract Machines
20090302	11	Unit Contacts
20090302	12	Tutorial Contacts
20090302	13	Lecturer Contact
20090302	14	Admin Contact
20090309	19	Unit Outline
20090401	20	Tutorial 2
20090402	24	Discussion Topic 2
20090406	25	Tutorial Exercises 3
20090407	26	Learning Module 6: Refinement - The Square Root Machine
20090415	27	Assignment 2
20090501	28	Discussion Topic 3
20090514	29	Admin Contacts
20090520	30	Discussion Topic 4
20090525	31	Examination
20090603	32	Learning Module 9: More Refinement - The Bridge Problem
20090603	33	Learning Module 10: Refinement Revisited
20090603	34	Learning Module 11: Sorting - algorithm and data refinement
20090616	35	Assignment 2 Solutions

Document History

20100301:101919	9.0.1	ajh	added `onlyB` resource
20100301:100939	9.0.0	ajh	first version for 2010

This page maintained by John Hurst.
Copyright Monash University Copyright Policy

37 accesses since
21 Jan 2010

Generated at 20100308:1710 from an XML file modified on 20100305:1110
Maintainer use only; not generally accessible: Local Server Work Server CSSE Server

134 accesses since 14 Feb 2010, HTML cache rendered at 20120524:2156