ÃÛÌÒ´«Ã½Æƽâ°æÏÂÔØ

Duration: 4Ìýhours

This module introduces basic concepts of functional verification and model checking. It demonstrates the importance of verification via some examples, outlines the challenges, and reviews pros and cons of model checking with respect to other verification methods.ÌýÌýÌýÌý

Duration: 5Ìýhours

This module introduces transition systems, a basic modeling formalism for representing behavior of hardware and software that is suitable for automated analysis. The syntax and semantics of transition systems are explained, and how sequential circuits can be represented as transition systems is described. Next, program graphs as a formalism to model software are introduced. Syntax of program graphs is described, and semantic interpretation using transition systems is explained.

Duration: 5Ìýhours

This module introduces some modeling formalisms capturing different types of system compositions. Particularly, interleaving of concurrent transition systems, compositions of systems communicating via shared variables or handshaking are explained. Additionally, synchronous parallelism is described for composing synchronous circuit composition.

Duration: 24Ìýhours

This module provides an opportunity to exercise modeling and composition formalisms and methods learned in the previous modules.

• Use skills from module 3 to find the transition system of systems using appropriate composition methods.
• Use skills from module 2 to construct circuit representations for sequential hardware designs, and derive the corresponding transition systems.
• Use skills from module 2 to find program graphs for individual threads of parallel systems and derive the corresponding transition systems.