Advertisement
Published in:
1997 | ReviewPaper | Chapter
Deductive verification of real-time systems using STeP
Authors : Nikolaj S. Bjørner, Zohar Manna, Henny B. Sipma, Tomás E. Uribe
Published in: Transformation-Based Reactive Systems Development
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.