• Calendar

November 26, Tuesday
12:00 – 14:00

Since its introduction in 1977 [Pnu77], the temporal logic approach to the specification and verification of reactive systems has matured into an engineering field, practiced in most of the leading VLSI designs industries such as Intel, IBM, Motorola, Siemens etc'. In this presentation I will first introduce the specification language of linear temporal language and the algorithmic verification method of symbolic model checking, used for the verification of finite-state systems. I then consider the problem of verifying infinite-state systems. These were traditionally verified by theorem provers. However, while algorithmic (automatic) verification methods are already being used in industry, theorem provers are considered impractical for the industrial environment. it is generally recognized that the only way formal verification can ever scale up to handle industrialize designs is by the extensive use of abstraction and modularization, which break the task of verifying a large system into several smaller tasks of verifying simpler systems. An interesting example is the problem of uniform verification of reactive parameterized systems: Given a reactive parameterized system $S(n): P[1] || ....|| P[n]$ and a temporal property $p$, verify that $S(n)$ satisfies p for every $n>1$. I present the method of network invariant that can be used to verify a wide spectrum of LTL properties, including liveness, using the industrial automatic tools of symbolic model checking.

The effectiveness of the network invariant method is illustrated on several examples, including a deterministic and probabilistic versions of the dining philosophers problem.