Verifying Industrial Control Software

Google Tech Talks
June, 4 2008

ABSTRACT

In this talk I will present the results of mathematically verifying third party flight control software. I will then present the results of mathematically verifying automatically generated code using The Mathworks code generation facilities and compare the cost against conventional development including V If time permits I will also present a small example of the form of the automatable formal verification of a specification in Simulink. The principles of the approach are generally applicable to other modelling languages that provide automatic code generation.

Speaker: Colin O’Halloran
Colin has worked in the area of Formal Methods for 25 years. He is a Visiting Professor at the University of York and a Visiting Fellow at Kellogg College Oxford University. He was a member of the European Space Agency’s Board of Inquiry into the failure of Arianne 5’s first flight.
His current interests are in the commercial assurance of software.

Duration : 0:37:27

[youtube UzGGJWPwi8g]