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.

Category:

People & Blogs

Tags:

• google
• techtalks
• techtalk
• engedu
• talk
• talks
• googletechtalks
• education

[Knife4kills]

fake and gay

[NPRCVI]

The specification of access time and the implementation of an online inquiry system. Minimum access time is more important for sequential usage of code. The dominant component of delay for sequential retrieval of records from data mining is the average time for a half rotation. The access time is, by guessing, and real time is controlled by the access provider. The memory devices and the processes still transfer data to the CPU. Google contains the master plan and rules the world wide web.