Developing UML-B for Avionics
The HiClass project is a consortium of industrial partners from the avionics domain supported by several universities including the University of Southampton.
The aim of the project is to improve the way the industrial partners use model-based development in the avionics domain.
To support the industrial partners, we are investigating methods and tool support for refining system level models to individual component specifications.
We are also improving the text-based user interface to provide new record structuring features. If you would like to hear more, please contact us.
Formalisation of State-chart models (with Sandia National Laboratories)
Sandia and Southampton are working together to introduce a notion of refinement and formal safety verification into the ‘run-to-completion‘ state-chart languages (such as SCXML) that are often used by design engineers.
To do this, we have developed tools to automatically translate SCXML state-chart models into UML-B models for formal verification.
The ‘run-to-completion‘ semantics introduces interesting challenges for both refinement and safety verification.
We have also utilised LTL model checking techniques for verifying behavioural properties of the model. If you would like to hear more, please contact us.
DB Netz
DB Netz are using UML-B as a route to formal verification of digital Railway Command Control and Signalling (CCS) system specifications. In the EULYNX initiative, SysML specification
models of CCS components have been developed such as an electronic interlocking and the corresponding field elements (point, signal, level crossing, etc.), describing their interfaces and how they communicate to make a safe railway system.
These models will be used for specifying component requirements to suppliers to provide interoperability. The functional requirements are specified by means of executable SysML state machines that are the basis for the creation of virtual prototypes.
That way the infrastructure managers of the railways participating in EULYNX can validate the specification by means of simulation without a profound
knowledge of the underlying specification language. The EULYNX MBSE approach has already led to significant improvement in the quality of
created specifications but still, it does not allow the formal verification of system properties.
Translating the SysML models into UML-B and hence Event-B brings mathematical precision
and allows system level safety properties to be proven, providing formal verification that the specification is safe.
If you would like to hear more, please contact us.
Modelling the Hybrid ERTMS Level 3 in UML-B
We used UML-B to model and verify the safety of a new European railway specification, Hybrid ERTMS Level 3. The specification is for a new kind of control system that will allow new trains that can communicate their position, to operate alongside older trains that rely on track detection equipment.
The control system splits the existing track sections into virtual sections so that the newer trains can be run at closer intervals, but reverts to using track detection in the presence of older rolling stock.
We used UML-B class diagrams to model the relationships between trains and track sections and state-machines to model the state of trains. Our model was constructed using nine refinement levels, culminating in a UML-B state-machine representing the control system of the specification.
The European railway specification was improved as a result of our verification results because we were unable to prove some safety properties in the initial version of the specification.
The ERTMS specification contains example scenarios to explain the meaning of the specification.
In order to check that our UML-B model reflects the behaviour described in the specification, we have developed a behaviour driven method and tools for animating scenarios in our model.
Using the Scenario Checker the tester chooses external events in the environment, while internal control events run automatically in response.
The scenarios can be saved and replayed to efficiently demonstrate the model behaviour at different levels of abstraction.
For more information about how the Scenario Checker can be useful to you, please don't hesitate to contact us
CODA Component Diagram models
CODA is a component modelling approach for rigorous hardware design, which has been developed at Southampton in collaboration with UK industry.
CODA includes a new kind of diagram that integrates with the UML-B tool suite. CODA provides an environment for modelling hierarchical components that communicate via timed channels.
The internal behaviour of the component can be modelled using embedded UML-B state-machines. The state-machine transitions can control, or be triggered by, the component’s port operations.
CODA also has a mechanism for decomposition so that complex models can be managed as a collection of independently refined and verified component models.
CODA integrates with hardware design automation flows through capabilities for generating VHDL hardware descriptions from CODA component models. The CODA tool suite is released open-source alongside the UML-B diagrammatic modelling tools.
If you would like to hear more, please contact us.