The Sovereign project deals with the verification of life-critical or safety-critical systems, a term that commonly refers to systems whose failure might endanger human life, lead to substantial economic loss, or cause extensive environmental damage.
There is no doubt that the future will dramatically increase the number of computer systems that we consider to be safety-critical. Therefore, the impact of these systems will be noticeable on many aspects of our life. As a result of this growing dependency, there is a consensus about the methodologies that should be followed in order to fulfill the safety requirements of these software systems: they all require the use of formal methods during the development cycle.
In a previous case study, performed on the authority of Rijkswaterstaat, we verified a vital part of the control software of the Maeslantkering, the storm surge barrier near the city of Rotterdam. Based on the lessons learnt from this case study and from similar verification experiments we aim to develop a general framework for the verification of safety-critical software, with which both functional correctness and security can be investigated.
The research will be performed in collaboration with Rijkswaterstaat and the Nuclear Research and consultancy Group, and involve case studies that continue the work on the Maeslantkering project and initiate new verification experiments with the Borssele Nuclear Power Station.
The Sovereign project is (partly) financed by the Netherlands Organisation for Scientific Research (NWO/TTW), and is supported by Rijkswaterstaat and the Nuclear Research Group.