Embedded Systems, MOSIG 2 (Option PDES), University of Grenoble

Edition 2011-2012

The course consists of two parts. The first part is taught by Florence Maraninchi. Please see the course homepage for more details. The second part is taught by me.

The second part of the course gives an introduction to a verification technique called model checking. We will consider the two temporal logics Computation Tree Logic (CTL) and Linear temporal logic (LTL) to express desired properties. LTL and CTL are the core of industrial logics like System Verilog Assertions (SVA) or Property Specification Language (PSL). Given a system and a desired property of the system (aka the specification), we will study algorithms that check if the system satisfies the property.

The second part of the course is structured as follows:

Slides and Course Material

Links to Related Topics


Examples of Industrial Verification Tools