Campus Event Calendar
Event Entry
New for: D3
What and Who
What Does V&V Actually Achieve?
John Rushby
SRI International - Menlo Park CA, USA
Talk
AG 1, AG 4, RG1, MMCI, AG 3, AG 5, SWS
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 15 March 2010
15:00
45 Minutes
E1 3
Lecture hall 001
Saarbrücken
Abstract
(Based on joint work with Bev Littlewood / City University UK)
The top-level goals for most critical systems are stated quantitatively--e.g., "no catastrophic failure in the lifetime of all airplanes of one type"--and these translate into probabilistic requirements for subsystems and hence for software--e.g., probability of failure less than 10-9 per hour for flight-critical software.
But V&V activities, such as those described in DO-178B for flight-critical software, are not about reliability, nor even safety: they specify practices that promote or assure correctness. Higher "Design Assurance Levels" or "Software Integrity Levels", which are required for the software of systems that have more stringent failure rates, generally stipulate additional V&V activities. But if V&V is about correctness, doing more of it presumably ensures the software is "more correct," not more reliable.
I will resolve these conundrums by arguing that what V&V actually does is provide evidence for assessing a probability of "possible perfection". Possible perfection does relate to reliability and has other attractive properties: for example, the possible perfection of one channel is conditionally independent of the failures of another, so the reliability of the whole system is the product of the probability of perfection of the first and the reliability of the second.
I will describe how formal verification can allow assessment of a probability of perfection, and will discuss plausible values for this probability and consequences for correctness of verification systems themselves.
The top-level goals for most critical systems are stated quantitatively--e.g., "no catastrophic failure in the lifetime of all airplanes of one type"--and these translate into probabilistic requirements for subsystems and hence for software--e.g., probability of failure less than 10-9 per hour for flight-critical software.
But V&V activities, such as those described in DO-178B for flight-critical software, are not about reliability, nor even safety: they specify practices that promote or assure correctness. Higher "Design Assurance Levels" or "Software Integrity Levels", which are required for the software of systems that have more stringent failure rates, generally stipulate additional V&V activities. But if V&V is about correctness, doing more of it presumably ensures the software is "more correct," not more reliable.
I will resolve these conundrums by arguing that what V&V actually does is provide evidence for assessing a probability of "possible perfection". Possible perfection does relate to reliability and has other attractive properties: for example, the possible perfection of one channel is conditionally independent of the failures of another, so the reliability of the whole system is the product of the probability of perfection of the first and the reliability of the second.
I will describe how formal verification can allow assessment of a probability of perfection, and will discuss plausible values for this probability and consequences for correctness of verification systems themselves.
Contact
Erich Reindel
--email hidden
passcode not visible
logged in users only
gk-sek, 03/05/2010 14:09
gk-sek, 03/05/2010 14:05 -- Created document.
gk-sek, 03/05/2010 14:05 -- Created document.