Abstract We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification’s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.

Fault localisation, i.e. the identification of program locations that cause errors, takes significant effort and cost. We describe a fast model-based fault localisation algorithm that, given a test suite, uses symbolic execution methods to fully automatically identify a small subset of program locations where genuine program repairs exist. Our algorithm iterates over failing test cases and collects locations where an assignment change can repair exhibited faulty behaviour. Our main contribution is an improved search through the test suite, reducing the effort for the symbolic execution of the models and leading to speed-ups of more than two orders of magnitude over the previously published implementation by Griesmayer et al. We implemented our algorithm for C programs, using the KLEE symbolic execution engine, and demonstrate its effectiveness on the Siemens TCAS variants. Its performance is in line with recent alternative model-based fault localisation techniques, but narrows the location set further without rejecting any genuine repair locations where faults can be fixed by changing a single assignment. We also show how our tool can be used in an educational context to improve self-guided learning and accelerate assessment. We apply our algorithm to a large selection of actual student coursework submissions, providing precise localisation within a sub-second response time. We show this using small test suites, already provided in the coursework management system, and on expanded test suites, demonstrating the scalability of our approach. We also show compliance with test suites does not reliably grade a class of “almost-correct” submissions, which our tool highlights, as being close to the correct answer. Finally, we show an extension to our tool that extends our fast localisation results to a selection of student submissions that contain two faults.

Computer science instructors need to manage the rapid improvement of novice programmers through teaching, self-guided learning, and assessment. Appropriate feedback, both generic and personalised, is essential to facilitate student progress. Automated feedback tools can also accelerate the marking process and allow instructors to dedicate more time to other forms of tuition and students to progress more rapidly. Massive Open Online Courses rely on automated tools for both self-guided learning and assessment.

Abstract PROB is an animation and model checking tool, which supports integrated event‐ and state‐based specifications combining B and CSP. We present an initial strategy for implementing the combined specification model as a concurrent Java program. Our Java implementation for the combined B and CSP model uses a similar approach to that of JCSP. The restricted operational semantics for the integrated B and CSP model in PROB is defined. Then a new Java package, JCSProB, is developed for implementing the semantics. The new package supports external choice with multi‐way synchronization, and introduces an improved multi‐threading implementation from JCSP. Copyright © 2009 John Wiley & Sons, Ltd.

The Mondex Electronic Purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment tower pattern is used to address one such issue in detail: the use of a hash function rather than a total injective function when clearing the highly constrained purse logs. A retrenchment is constructed from the lowest level model to a model using a hash, and is then lifted to create two refinement developments, working at different levels of detail, and connected via retrenchments. The tower development is appropriately validated, vindicating the design used.

The Mondex electronic purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment tower pattern is used to address one such issue in detail: the finiteness of the purse log (which records unsuccessful transactions). A retrenchment is constructed from the lowest level model of the purse system to a model in which logs are finite, and is then lifted to create two refinement developments of the purse, working at different levels of detail, and connected via retrenchments, forming the tower. The tower development is appropriately validated, vindicating the design used

Simple retrenchment is briefly reviewed in the B specification language of J.-R. Abrial (1996) as a liberalization of classical refinement, for the formal description of application developments too demanding for refinement. The looser relationships allowed by retrenchment between adjacent models in the development process may capture some of the requirements information of the development. This can make requirements validation more difficult to understand since the locus of requirements should be the models, and not their interrelationships, as far as possible. Hence the universal construction by Banach (2000), originally proposed for simple transition systems, is reformulated in B, in order to "lift" a given retrenchment conceptually, thus retracting such requirements information back to the level of abstraction of the abstract, ideal model. Examples demonstrate the cognitive value of retracting requirements to the abstract level, articulated in a well-understood formal language. This is also seen to yield a more understandable way of comparing alternative retrenchment designs. Some new B syntax in the pre- and postcondition style is presented to facilitate expression of the lifted requirements.

Retrenchment is presented in a simple relational framework as a more flexible development concept than refinement for capturing the early preformal stages of development, and briefly justified. Fragmented retrenchment permits the granularity of actions to decrease across a development step, many concrete steps retrenching a single abstract one. This generates the usual proliferation of interleavings of events at the concrete level. Event structures, particularly flow event structures, help to control these within the retrenchments of a single abstract step, while the concurrent reading of the fragmented retrenchment proof obligation permits acceptable interleavings of retrenchments of different steps. It is observed that retrenchment allows the convenient description of unfair behaviours when fairness is not guaranteed.

Discusses a simple example that demonstrates various expressive limitations of the refinement calculus, and suggests a liberalization of refinement, called retrenchent, which supports an analogous formal development calculus. Useful concrete system behaviour can be specified outside the domain of pure refinement, and a case is made for fluidity between I/O and state components across the development step. A syntax and a formal definition are presented for retrenchment, which has some necessary properties for a formal development calculus: transitivity gives stepwise composition of retrenchments, while monotonicity w.r.t. the specification language constructors gives piecewise construction of retrenchments.

Abstract. Sharp retrenchment is introduced and brie y justified informally, as a liberalisation of refinement. In sharp retrenchment the relationship between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing most particularly the description of non-refinement-like properties, and the mixing of I/O and state aspects in the passage between levels of abstraction. Sharp retrenchments are brie y contrasted with unsharp ones. Sharp retrenchments are shown to have a natural law of composition, and the way in which refinements may be viewed as sharp retrenchments is discussed. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between sharp retrenchment and refinement, and various notions of simulation are considered in this context, specifically: stepwise simulation, the ability of simulator to mimic a sequence of execution steps of the simulatee; strong simulation, in which states and step labels are mapped independently between simulatee and simulator; and the refinement notion itself. Special cases of sharp retrenchment are shown to possess various subsets of these simulation properties, and the extent to which sharp retrenchments contain refinements within them is addressed. The details of the theory are worked out for the B-Method, though the applicability of the underlying ideas is not limited to just that formalism.