High Integrity Systems (CS_313)/Critical Systems (CS_M13)

Michaelmas Term 2009

Lecturer

Slides, Handouts

• In order to read and print out pdf-files, you need a PDF reader. For instance Acrobat Reader is available free here:
• For my students: Please don't print these files on departmental printers. Instead ask in the student secretary for a copy. To print out on ordinary printers costs, because of the cost of the toner, 5 to 10 times more than fotocopying, as done by the lecturer.
• Slides by section
  • Errata
    • Postscript
    • Pdf
  • Section 0
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 1
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 2
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 3
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 4
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 5
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 6
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 9
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing

Programming Examples

• SPARK_Ada Examples (See README file for instructions on how to use Spark Ada and ada)

Links

• Module given in previous years
  • Course page Critical Systems CS_M13 from 2008/09
  • Course page Critical Systems CS_M13 from 2004/05
  • Course page Critical Systems CS_M13 from 2003/04
  • Course page Critical Systems CS_411 from 2002/03
  • Course page Critical Systems CS_411 from 2001/02
• Programming Errors
  • BBC News: Top 25 Programming Errors
• Ada
  • S. Barbey, M. Kempe, and A. Strohmeier: Object-Oriented Programming with Ada 9X
  • Ada95 Lovelace Tutorial
• Examples of failures of critical systems.
  • Therac-25
    • Therac-25: The treatment that killed
    • A history of the introduction and shut down of Therac-25
• Ethics
  • The Software Engineering Code of Ethics and Professional Practice
  • The ACM Code of Ethics and Professional Conduct Software Engineering Code of Ethics and Professional Practice (Version 5.2) as recommended by the IEEE-CS/ACM Joint Task Force on Software Engineering Ethics and Professional Practices
  • Ethics
  • Ethics of Safety Critical Systems
• B Method
  • B method was used in verifying a new driverless train line on the Paris metro (the web pages don't report any details)
    • Siemens - Paris Metro
    • link b