An Approach to Modelling and Refining Timing Properties in B
Michael J. Butler, Jérôme Falampin · ePrints Soton (University of Southampton) · 2002
Introduction The work described in this extended abstract is being undertaken as part of the EU-funded MATISSE project (IST-1999-11435). One of the major case studies of MATISSE involves the application of the B Method [2] to a railway control system. The emphasis of the work is on system-level modelling and analysis. This means we are not just modelling pieces of control software in B, but we are using B to model relevant aspects of an entire network. For example, a system-level model would include physical connections between track sections, the positions of trains in terms of the sections they currently occupy, and under what system-level conditions the emergency brakes should be applied to ensure safety. This system-level model has been decomposed and refined into distributed trackside and on-board controllers with messages passing between them. This allows us to derive the software specifications for the individual controllers in a way that increases our confidence that the combi