Find out more Talk to our research team and find out more about this work. Professor Michael Butler led the research on this project.
Staff profile
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.
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 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.
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.
Talk to our research team and find out more about this work. Professor Michael Butler led the research on this project.
Telephone: +44 (0) 23 8059 44 (0) 7542799608
Email: I.Ullah@soton.ac.uk
University of Southampton student Curtis Parfitt-Ford has been honoured at the TARGETjobs Undergraduate of the Year Awards for action that forced a Government U-turn on the A-level grading algorithm.
The first year BSc Computer Science student spearheaded a legal challenge against August's proposed algorithm that, for class sizes larger than 15, determined grades based on schools' past performance rather than individual achievement.
His powerful efforts, partnered with legal specialists at Foxglove, have been recognised with The Young Activist of the Year Award.
"The A-level algorithm scandal brought issues of algorithmic justice into the public consciousness, with it touching so many lives across the country," Curtis says. "It's an honour and a privilege to have our challenge recognised, and I can only hope that it leads to a greater public conversation and dialogue about oversight of algorithmic decision-making more broadly."
Last summer, UK students did not sit exams because schools were closed during the coronavirus lockdown. In England, grades were decided by the official exam regulator, Ofqual, who proposed an algorithmic model that factored in estimated grades, teacher rankings and schools' past performance.
"This policy was discriminatory," Curtis says, "with bright students in worse-off areas being punished; it was illogical, as the Government had already admitted that teachers were the ones who knew their students' performance best; and it was illegal, as it automatically profiled hundreds of thousands of students across the country without any way of opting out or requesting manual review.
"When I learned that this was happening, the Friday before results day, I knew that I couldn't sit around and let it pass: I could see the impact that it would have on so many across the country. Yet, when I started reaching out to lawyers, I'd never have imagined that we'd force the Government to back down and U-turn in just over a week."
In a matter of days, the campaign raised more than £30,000 to cover potential adverse costs, and more than a quarter of a million people signed a petition Curtis started to Ofqual.
"I'm so incredibly grateful to everyone who signed the petition, who contributed to our crowdfunder, and who helped us make the noise we did about our case," he says.
Curtis is the Technical Officer of the University's LGBTQ+ Society, as well as the Events Lead for its St John Ambulance unit. He also runs a company called Loudspeek, which enables progressive political campaigns to put supporters in touch with their representatives.
"I'm fascinated by the intersection of law and technology, and think the two absolutely have to go together," he says. "Where law lags behind tech, we can see huge injustice, and where tech has to wait for the law to catch up, we risk losing out on revolutionary innovation. Computer science, and the whole Electronics and Computer Science (ECS) field more broadly, offers a huge amount of power - and yet, that power necessarily must come with responsibility.
"As easy as it is for a teenager in their bedroom to invent a website that reinvents the way we interact for good, it's equally easy for people who are genuinely well-intentioned to make systems that are rife with bias, that are inaccessible, or that exacerbate existing inequalities in our society. It's so important that all those implications are thought through and challenged when they're not working how they should - that's the space I'd love to end up working in ultimately."
The Young Activist of the Year Award is partnered by Clifford Chance and One Young World.