Europe relies on the availability and flawless functioning of distributed infrastructure services such as electricity, water, communication, transportation and environmental management, which are all increasingly controlled by software. Currently, however, the potential for innovation is limited owing to the inherent risks and costs of upgrades. For example, incompatibilities when simultaneously running old and new versions of control software can result in major service outages. Similarly, fast moving technology, such as sensors, could enable advances in safety critical applications such as aerospace; however revalidating avionics software to introduce new niche functionality is prohibitively expensive. The PINCETTE project has been set up specifically to ensure safe infrastructure upgrades and enable rapid product development by providing solutions for continuous validation. Certainty in the safety of upgrades will allow communities to confidently apply and leverage the efficiency gains and advantages of upgrades.
The Electricity National Control Centre for Great Britain. Photo: National Grid.
The PINCETTE project targets the problem of analyzing and validating complex systems upgrades. London’s power grid, for instance, has over 4000 medium-voltage substations; the software in controllers for these substations must prevent power outages and ensure safety. A malfunctioning device can result in huge economic damage and can even threaten human lives. Upgrades to software might be needed to improve efficiency or to fix a bug, but validating this upgrade is complicated owing to the software being distributed across substations and the entire grid. Additionally, the grid cannot be switched off when validating an upgrade, making upgrades across such a network a huge safety concern.
With current technology, the only option is to supplement each incremental change or upgrade in the system with a complete revalidation of the whole system, incurring enormous cost in the process. The need to conduct total system checks arises from the fact that state-of-the-art testing and formal verification tools are not optimized to validate system changes and upgrades, but instead focus on a single program version only. For instance, in a new release of software or an operating system, bugs are often found post release and patches are then distributed. However, this approach which relies on the discovery of bugs created by upgrades during use of the product and subsequently fixing them is not acceptable in many domains, particularly safety critical systems such as aerospace, medical devices, nuclear reactors etc, when it is crucial to ensure the absence of bugs for every upgrade. The associated cost can lead to a very conservative attitude to changes and a failure to fully exploit potentially beneficial advances in technology.
In the PINCETTE project, we are working towards resolving this problem by developing the technology to ensure safe infrastructure upgrades by validating continuously evolving networked software systems. Our goals are to 1) reduce the cost and time to market of upgrades by several orders of magnitude; 2) increase the level of confidence in the safety of upgrades; 3) enable certification of upgrades. The notion of ‘system upgrade’ in PINCETTE is broad and includes changes of functionality, bug fixes, feature upgrades, and requirement changes.
In the PINCETTE approach for upgrade validation, we do not revalidate the new version of the system in its entirety. Instead we only verify the safety of the portion of the system affected by the upgrade and the impact of the upgrade on the new version. This is done by utilising the knowledge that the behavior of the existing version of the system is safe. Doing this will drastically reduce the time and effort required to revalidate the new version and result in dramatic cost savings. To achieve this, we are developing technologies to assess the impact of changes. We plan to use a combination of state-of-the-art static and dynamic analysis techniques for efficient analysis of system changes. Dr Hana Chockler's team at IBM Haifa, Prof Daniel Kroening’s group at the University of Oxford, Prof Natasha Sharygina’s group at Universita Della Svizzera Italiana (USI) and Dr Leonardo Mariani’s group at Universita' Degli Studi Di Milano-Bicocca (UniMiB) are working together to develop the technology for change impact analysis and verification. The tools developed will be tested and validated on real world systems:
- A UAV (Unmanned Air Vehicle) observation payload example provided by IAI (Israeli Aerospace Industries)
- Software for high-voltage and medium-voltage substation automation systems offered by ABB
- A control system for remote maintenance operations of the ITER fusion reactor provided by VTT (The Technical Research Centre of Finland).
The project commenced in July 2010 and will run for three years under funding from FP7 ICT-2009.1.4 Trustworthy ICT.
Department of Computer Science,
University of Oxford
Tel: +44 1865 610736