BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:What is Software Assurance? - John Rushby\, SRI International
DTSTART:20110412T151500Z
DTEND:20110412T161500Z
UID:TALK30348@talks.cam.ac.uk
CONTACT:Wei Ming Khoo
DESCRIPTION:Safety-critical systems must be supplied with strong assurance
  that they are\, indeed\, safe.  Top-level safety goals are usually stated
  quantitatively--for example\, "no catastrophic failure in the lifetime\no
 f all airplanes of one type"--and these translate into probabilistic requi
 rements for subsystems\, and hence for software. In this way\, we obtain q
 uantitative reliability requirements for software: for example\, the proba
 bility of failure in flight-critical software must not exceed 10-9 per hou
 r.\n\nBut the methods by which assurance is developed for critical systems
  are mostly about correctness (inspections\, formal verification\, testing
  etc.) and these do not seem to support quantitative reliability claims.  
 Furthermore\, more stringent reliability goals require more extensive corr
 ectness-based assurance.  How does more assurance of correctness deliver g
 reater reliability?\n\nI will resolve this conundrum by arguing that what 
 assurance actually does is provide evidence for assessing a probability of
  "possible perfection."  Possible perfection does relate to reliability an
 d has\nother attractive properties that I will describe.  In particular\, 
 it allows assessment of the reliability of certain fault-tolerant architec
 tures.  I will explain how formal verification can allow assessment of a p
 robability of perfection\, and will discuss plausible values for this prob
 ability and consequences for correctness of verification systems themselve
 s.\n\nThis is joint work with Bev Littlewood of City University\, London U
 K.
LOCATION:Lecture Theatre 2\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR