Project Abstract

Motivating by the issues in software development like high costs in development, maintainability, and testing especially for safety-critical software which makes them more expensive. Developing a traffic control systems as a safety-critical system using language and methods like Uppaal ,Ada ,python ,C/C and soon is leading to safety risks and high maintenance costs. The core proposition of this study is to development of a traffic control system that prevents the island from being swamped by cars using the B method and Atelier B IDE. Unlike the conventional approach (Uppaal,Ada,python ), the B method way of development helps to detect errors in the early development stages and this can reduce cost and time for testing and not need any maintenance costs. As errors can come from the compiler or IDE we are using for development, so using Atelier B which is designed to produce zero-defect software reduces compiling errors and testing time by replacing unit testing by large mathematical proofs. The development cycle begins with an abstract specification and refining it through successive stages to a concrete or implementable model. By leveraging the Atelier B toolset, at each stage of the development proof of obligations (POs) are generated to guarantee the validity of the refinement and the consistency of the abstract machine. This traffic control system manages the traffic light cycle, no excessive number of cars entered into the island and having a final model that successfully passes all the proof of obligations. This work contributes formally verified traffic control system using the B Method which is recommended for the development of critical systems as its future of layered development, using mathematical proofs for testing and early detection of errors.

Keywords: The B method, Safety critical systems, Traffic control system

 Conference Details

Session: B

Location: Sir Stanley Clarke Auditorium at 13:30 15:30

Markers: Markus Roggenbach, Sean Walton

Course: BSc Computer Science 3yr FT

Future Plans: I’m looking for work