This course provides a deeper understanding of both deductive and algorithmic methods and tools for ensuring the safety and correctness of mission critical systems (e.g. medical devices such as pacemakers, nuclear reactors and train control systems). In addition to deductive techniques, the course treats algorithmic methods such as model-checking tools, specification languages such as temporal logic, table based specification methods, and the nature of software certification.
- The ability to explain the importance of safety-, mission-, business-, and security-critical systems.
- Demonstrated knowledge of the importance of good software engineering practices for critical systems.
- The ability to use rigorous software engineering methods to develop dependable software applications that are accompanied by certification evidence for their safety and correctness.
- Knowledge of the method and tools using deductive approaches (such as theorem proving).
- Knowledge of methods and tools for algorithmic approaches (such as model checking, bounded satisfiability) etc.
- Knowledge of the theory underlying deductive and algorithmic approaches.
- The ability to use industrial strength tools associated with the methods on large systems.