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.