Citation
Edward A. Lee. "Verifying Real-Time Software Is Not Reasonable (Today)". Talk or presentation, 24, April, 2013; Invited talk.

Abstract
Verification is about demonstrating that a formal system holds certain properties. It is particularly important to verify safety-critical real-time control software, such as aircraft or automotive control systems. Unfortunately, many of the properties that need to be verified for such systems are not actually part of the formal system defined by the software. It therefore makes no sense to verify the software. So what should be verified? It is glib to say that ”the system” must be verified, because ”the system” is not a formal system. It is a bundle of silicon and wires. Only a model of the system can be verified. What model?

If the semantics of software is extended to include temporal properties, then verifying real-time software becomes possible. In this talk, I will argue that such extensions are practical and effective, but that they require rethinking software abstractions at a rather fundamental level. Moreover, they require reengineering of many performance optimizations that computer architects, compiler designers, and operating system designers have instituted. I will show for some of these that such engineering yields designs that have competitive performance and verifiable timing. 

Electronic downloads

• 78570002.pdf · application/pdf · 1485 kbytes

• HTML

  Edward A. Lee. <a
  href="http://chess.eecs.berkeley.edu/pubs/988.html"
  ><i>Verifying Real-Time Software Is Not Reasonable
  (Today)</i></a>, Talk or presentation,  24,
  April, 2013; Invited talk.

• Plain text

  Edward A. Lee. "Verifying Real-Time Software Is Not
  Reasonable (Today)". Talk or presentation,  24, April,
  2013; Invited talk.

• BibTeX

  @presentation{Lee13_VerifyingRealTimeSoftwareIsNotReasonableToday,
      author = {Edward A. Lee},
      title = {Verifying Real-Time Software Is Not Reasonable
                (Today)},
      day = {24},
      month = {April},
      year = {2013},
      note = {Invited talk.},
      abstract = {Verification is about demonstrating that a formal
                system holds certain properties. It is
                particularly important to verify safety-critical
                real-time control software, such as aircraft or
                automotive control systems. Unfortunately, many of
                the properties that need to be verified for such
                systems are not actually part of the formal system
                defined by the software. It therefore makes no
                sense to verify the software. So what should be
                verified? It is glib to say that �the system�
                must be verified, because �the system� is not
                a formal system. It is a bundle of silicon and
                wires. Only a model of the system can be verified.
                What model? <p> If the semantics of software is
                extended to include temporal properties, then
                verifying real-time software becomes possible. In
                this talk, I will argue that such extensions are
                practical and effective, but that they require
                rethinking software abstractions at a rather
                fundamental level. Moreover, they require
                reengineering of many performance optimizations
                that computer architects, compiler designers, and
                operating system designers have instituted. I will
                show for some of these that such engineering
                yields designs that have competitive performance
                and verifiable timing. },
      URL = {http://chess.eecs.berkeley.edu/pubs/988.html}
  }
  

Posted by Mary Stewart on 24 Apr 2013.
Groups: actionwebs
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.