When it comes to designing software for the computer systems used in safety-critical sectors, reliability is paramount. Drawing on sophisticated mathematical modelling and analysis techniques, researchers at Southampton have developed a set of open-source tools to support robust software design in industries such as aerospace, rail and defence. The toolset is being used by companies around the world, saving time and money and boosting innovation.
Research challenge and context
When developing or modifying software, engineers can use formal methods – a range of mathematical techniques for modelling the software and testing how it will work – to detect and prevent errors at every stage of the process. These methods of validation (checking that the software specification meets the user requirements) and verification (ensuring that the software works correctly, satisfying the specification) are crucial in contexts such as transport or aerospace, where failure could have catastrophic results.
Existing formal methods provide rich mathematical languages for modelling and reasoning about correct system behaviour. However, it is difficult to scale them for complex systems in which a software-based controller manages many features or controls a large proportion of a system’s functions – for example, a control system that supervises a large volume of traffic on a rail network.
Another issue with formal methods approaches is slow uptake in industry, where the potential improvements in reliability, and savings in testing and reworking costs, are not always recognised and the techniques are perceived as being inaccessible to non-academic engineers.
Our solution
Our researchers have developed a set of open-source formal modelling and verification tools to support robust software design in industries such as aerospace, rail and defence.
Working in collaboration with several European universities, Southampton researchers developed Rodin, a design tool capable of the verification and validation (V&V) of complex software systems.
Rodin’s core features are open source, allowing academic research groups to develop and experiment with new V&V features. However, to support the adoption of the technology in industry, the researchers developed ‘industrial strength’ plug-ins. One of these, UML-B, is an interface that provides a graphical representation of the models, making the modelling language easier to understand and more user friendly.
Another plug-in, ProB, enables engineers to add a powerful form of mathematical reasoning, called model checking, to the V&V process. Formal methods use two types of computer-based reasoning, model checking and automated deduction. Automated deduction is a logic-based approach that can scale to models with large dimensions but is not fully automatic and requires some human intervention to guide the reasoning. Model checking provides a completely automatic approach to finding design errors by restricting the dimensions of a model. Typically, formal methods tools only support one type of reasoning. ProB extends the automated deduction provided by Rodin with model checking capability, enabling engineers to use both approaches.
What was the impact?
Engineers in companies worldwide, including AWE in the UK and Thales in Austria, are successfully using Rodin in the early-stage design and validation of computer-based control systems. The toolset is helping them uncover potential design problems earlier in the development of new systems, contributing to safer system design and avoiding expensive reworkings.
Through University consultancy ECS Partners, the research team has delivered Rodin training and customisation services to a range of companies, including AWE, Sandia Labs, Thales, Deutsche Bahn and Hitachi. In addition, the Rodin toolset is being used for academic research and undergraduate and postgraduate teaching in universities worldwide.
The research team has nurtured an international community of Rodin users and developers. As an open-source toolset, free to use for research and commercial purposes, the 2018 version of Rodin has been downloaded over 10,000 times, and Southampton hosts a well-used online resource providing user and developer support. Since 2009, the University has organised Rodin workshops that attract users and developers from around the globe.
Find out more
Talk to our research team and find out more about this work. Professor Michael Butler led the research on this project.