Library

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    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
    Keywords: temporal logic ; deductive verification ; verification diagrams ; model checking
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: 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.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1008700623084
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    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
    Keywords: Keywords: Model checking; STeP; Verification; Verification diagrams
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: 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.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s001650070014
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Verification of clocked and hybrid systems (2000)
    Springer
    Acta informatica 36 (2000), S. 837-912 
    Details
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: 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.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s002360050177
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Book
    Book
    Mathematical Theory of computation (2003)
    Mineola, New York :Dover,
    Details
    Title: Mathematical Theory of computation
    Author: Manna, Zohar
    Edition: Unabr. republication of the work originally publ. by McGraw-Hill Book Comp., NY in 1974
    Publisher: Mineola, New York :Dover,
    Year of publication: 2003
    Pages: X, 448 S.
    ISBN: 0-486-43238-6
    Type of Medium: Book
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    ZIB Catalog
    Zuse Institute Berlin get availability status
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...