The work of ADVANCE is being driven by two major industrial case studies, one on railway interlocking and the other on smart energy grids.
Railway Case Study - Lead: Alstom
The purpose of the ADVANCE Railway case study is to investigate an approach for the safety validation of Interlocking systems (IXL) that form, set and lock safe routes for trains within switching stations. We propose an approach that ensures train safety by introducing a software layer which filters out any IXL commands leading to a hazardous situation. This application, called the interlocking dynamic controller (IXL-DC), allows outputs of the interlocking to be controlled dynamically. The controller is positioned between the interlocking and the physical outputs. The IXL-DC will authorise delivery of IXL system outputs if and only if they satisfy IXL safety properties.
Current practice in the railway industry involves verification of specific interlocking configurations based on fixed track layout and route data. We aim to develop an approach based on verification of generic models of interlocking using ADVANCE methods and tools. The proposed solution relies on mathematical proof of generic Event-B models taking into account safety requirements and is independent from the size and complexity of particular switching stations and from the behaviour of the execution engine of interlocking systems.
The objectives of the case study are to demonstrate the technical feasibility of the proposed solution, to define a process involving ADVANCE methods and tools that would permit certification of the final product in a cost effective way based on reusable verified formal models and to support the consortium in bringing the ADVANCE methods and tools to a technology readiness level permitting to develop the solution in an industrial context. Safety certification is the main driver for the use of formal methods in the railways domain and the development of a strategy for future use of ADVANCE methods and tools in certification is an important goal.
Smart Grid Case Study - Lead: Critical Software Technologies
The differentiating factor of a smart grid in comparison to existing energy grids is the two-way communication between the consumer and supplier. This presents the opportunity for the consumer to have a more dynamic role in managing their energy use; by having access to up-to-date energy records and the option to switch between different rates and energy plans. It also allows for a more efficient and intelligent system on the supplier side; which can work around high demand and power outages by constantly updating the price and availability by considering the activity on the rest of the grid. The result is a reduction in the cost and waste of energy for both parties.
The proposition of the ADVANCE Smart Grid case study is to verify the security and reliability of the communication infrastructure on the distribution network of a smart grid system. In particular the case study is going to verify properties associated with low voltage substations system, data centre and smart metres. An important aspect that is being modelled is the data interchange between the consumers, suppliers and other native devices in the network. Formal methods present an ideal means of achieving this goal and establishing a best practice as the technology surrounding smart grid systems is still fairly loosely defined and attracts high development costs throughout the life cycle due to the traditional development methods used.
The modelling strategy in the Smart Grid case study is based heavily upon the idea of decomposition. The combined system naturally lends itself to decomposition into separate models for the data centre, network, and monitoring/control units (in this case the SIU). Each of these models are developed independently and then composed again at later points to check that the composed system is a refinement of the original combined system. This is a suitable approach for distributed networks in general - and provides a strategy which can be reused - as the model for the combined system will be the same for any system of this type. It is only when work begins on the separate decomposed models that the attributes specific to each system are introduced.
