Anzeige
Erschienen in:
1997 | ReviewPaper | Buchkapitel
Deductive verification of real-time systems using STeP
verfasst von : Nikolaj S. Bjørner, Zohar Manna, Henny B. Sipma, Tomás E. Uribe
Erschienen in: Transformation-Based Reactive Systems Development
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.