Verifying Temporal Properties of Reactive Systems: A STeP Tutorial |
| |
| Authors: | Nikolaj S Bjørner Anca Browne Michael A Colón Bernd Finkbeiner Zohar Manna Henny B Sipma Tomás E Uribe |
| |
| Affiliation: | (1) Computer Science Department, Stanford University, Stanford, California 94305, USA;(2) Computer Science Department, Stanford University, Stanford, California 94305, USA |
| |
| Abstract: | We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction. |
| |
| Keywords: | temporal logic deductive verification verification diagrams model checking |
| 本文献已被 SpringerLink 等数据库收录！ |
|
