@www.csse.monash.edu.au |
| Assessment | Contacts | Lectures | Resources | Timetables | Tutorials | Unit Outline |
| Last modified: 20090330:171710/updated Sample Machines section | FIT3013 AJH-2009-09 |
MUSO | Books | Lecture Slides | Event-B Resources | Web Documents
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/2009/. 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).
The prescribed text book is:
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.
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.
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.
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.
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.
Some of these machines are described in lectures.
| Date | Machine |
|---|---|
| 20090316 | The Bridge Context, refinement 0 The Bridge Machine, refinement 0 |
| 20090330 | The Simple Library Context The Simple Library Machine |
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
A similar paper is also at http://www.bmethod.com/dl/thierry_lecomte/TL_FM2008_Metro_Platform_Screen_Doors_Control_Command_Systems.pdf
| 20090330:171710 | 8.0.1 | ajh | updated Sample Machines section |
| 20090205:134819 | 8.0.0 | ajh | first version for 2009 |
| This page maintained by John Hurst. Copyright Monash University Copyright Policy |
|   | |
Generated at 20090703:0843 from an XML file modified on 20090330:1717 | |||