Bibliothek

X
Sie haben 0 gespeicherte Treffer.
Markieren Sie die Treffer und klicken Sie auf "Zur Merkliste hinzufügen", um sie in dieser Liste zu speichern.
feed icon rss

Ihre E-Mail wurde erfolgreich gesendet. Bitte prüfen Sie Ihren Maileingang.

Leider ist ein Fehler beim E-Mail-Versand aufgetreten. Bitte versuchen Sie es erneut.

Vorgang fortführen?

Exportieren
Filter
  • 2000-2004  (4)
  • 1
    Digitale Medien
    Digitale Medien
    Verifying Temporal Properties of Reactive Systems: A STeP Tutorial (2000)
    Springer
    Formal methods in system design 16 (2000), S. 227-270 
    Details
    ISSN: 1572-8102
    Schlagwort(e): temporal logic ; deductive verification ; verification diagrams ; model checking
    Quelle: Springer Online Journal Archives 1860-2000
    Thema: Informatik
    Notizen: 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.
    Materialart: Digitale Medien
    URL: http://dx.doi.org/10.1023/A:1008700623084
    Bibliothek Standort Signatur Band/Heft/Jahr Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    Artikel (Nationallizenzen)
    Volltext
  • 2
    Digitale Medien
    Digitale Medien
    The ‘Cash-Point’ Service: A Verification Case Study Using STeP (2000)
    Springer
    Formal aspects of computing 12 (2000), S. 218-219 
    Details
    ISSN: 1433-299X
    Schlagwort(e): Keywords: Model checking; STeP; Verification; Verification diagrams
    Quelle: Springer Online Journal Archives 1860-2000
    Thema: Informatik
    Notizen: Abstract. STeP, the Stanford Temporal Prover, supports the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB99]. Automated model checking is combined with computer-aided deductive methods to allow for the verification of a broad class of systems, including parameterised (N-component) circuit designs, parameterised (N-process) programs, and programs with infinite data domains.
    Materialart: Digitale Medien
    URL: http://dx.doi.org/10.1007/s001650070014
    Bibliothek Standort Signatur Band/Heft/Jahr Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    Artikel (Nationallizenzen)
    Volltext
  • 3
    Digitale Medien
    Digitale Medien
    Verification of clocked and hybrid systems (2000)
    Springer
    Acta informatica 36 (2000), S. 837-912 
    Details
    ISSN: 1432-0525
    Quelle: Springer Online Journal Archives 1860-2000
    Thema: Informatik
    Notizen: Abstract. This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety a nd liveness properties of clocked transition systems. All rules are associated with verification diagrams. The verification of response properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for u ntimed reactive systems, for proving all interesting properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTS isnon-zeno. Finally, we present an extension of the model and the invariance proof rule for hybrid systems.
    Materialart: Digitale Medien
    URL: http://dx.doi.org/10.1007/s002360050177
    Bibliothek Standort Signatur Band/Heft/Jahr Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    Artikel (Nationallizenzen)
    Volltext
  • 4
    Buch
    Buch
    Mathematical Theory of computation (2003)
    Mineola, New York :Dover,
    Details
    Titel: Mathematical Theory of computation
    Autor: Manna, Zohar
    Ausgabe: Unabr. republication of the work originally publ. by McGraw-Hill Book Comp., NY in 1974
    Verlag: Mineola, New York :Dover,
    Erscheinungsjahr: 2003
    Seiten: X, 448 S.
    ISBN: 0-486-43238-6
    Materialart: Buch
    Bibliothek Standort Signatur Band/Heft/Jahr Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    ZIB Katalog
    Zuse-Institut Berlin get availability status
Schließen ⊗
Diese Webseite nutzt Cookies und das Analyse-Tool Matomo. Weitere Informationen finden Sie hier...