Anyone who has ever designed an embedded system or a communication protocol involving several components executing simultaneously knows that such software is inherently susceptible to bugs. Typical problems include race conditions, deadlocks, and unexpected interplay between different components. The parallel nature of these systems makes it notoriously hard to detect such bugs using testing (timing, e.g., plays a crucial role). This course is designed to provide an introduction to the problems that arise in the design of such systems. It provides ways to model such systems and reason about them.
Objectives:
The purpose of this course is to learn how to specify the behavior of embedded systems, and to experience the design of a provably correct system. In this course you will learn how to formally specify requirements, and to prove or disprove them on the behavior. You will experience how to apply the techniques in practice in a practical assignment.
