About

The course covers techniques for developing high assurance systems -- systems that are safety critical, security critical, or mission critical in nature. In contrast to general purpose systems, high assurance system development tends to place a more stronger emphasis on rigorous requirements and specifications, verification and validation, and certification. In particular, high assurance system development is more likely to be amenable to formal verification techniques -- techniques that use various forms of machine-checkable mathematics or logic to demonstrate that a system satisfies its specification. The goal of this course teach techniques for writing requirements and formal specifications and for automated checking that a system conforms to its specification. These techniques will be illustrated using industrial relevant examples.