caa a22 4500 475797515 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000601xx s 000 0 eng 10.1023/A:1008700623084 doi (NATIONALLICENCE)springer-10.1023/A:1008700623084 Verifying Temporal Properties of Reactive Systems: A STeP Tutorial [Elektronische Daten] [Nikolaj Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomás Uribe] 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. Kluwer Academic Publishers, 2000 temporal logic nationallicence deductive verification nationallicence verification diagrams nationallicence model checking nationallicence Bjørner Nikolaj Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Browne Anca Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Colón Michael Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Finkbeiner Bernd Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Manna Zohar Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Sipma Henny Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Uribe Tomás Computer Science Department, Stanford University, 94305, Stanford, California, USA aut Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 227-270 0925-9856 16:3<227 2000 16 10703 https://doi.org/10.1023/A:1008700623084 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008700623084 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Bjørner Nikolaj Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Browne Anca Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Colón Michael Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Finkbeiner Bernd Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Manna Zohar Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Sipma Henny Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 700 1- Uribe Tomás Computer Science Department, Stanford University, 94305, Stanford, California, USA aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 227-270 0925-9856 16:3<227 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer