Skip to main content
SpringerLink
Log in

Formal Systems Specification

The RPC-Memory Specification Case Study

  • Conference proceedings
  • © 1996

Overview

Editors:
  1. Manfred Broy
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Stephan Merz
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Katharina Spies
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1169)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (17 papers)

  1. Front Matter

    Download chapter PDF

  2. The RPC-memory specification problem problem statement

    • Manfred Broy, Leslie Lamport
    Pages 1-4

  3. The RPC-memory case study: A synopsis

    • Manfred Broy, Stephan Merz, Katharina Spies
    Pages 5-20

  4. A TLA solution to the RPC-memory specification problem

    • Martín Abadi, Leslie Lamport, Stephan Merz
    Pages 21-66

  5. A dynamic specification of the RPC-memory problem

    • Egidio Astesiano, Gianna Reggio
    Pages 67-108

  6. A memory module specification using composable high-level petri nets

    • Eike Best
    Pages 109-159

  7. Constraint oriented temporal logic specification

    • Johan Blom, Bengt Jonsson
    Pages 161-182

  8. A functional solution to the RPC-memory specification problem

    • Manfred Broy
    Pages 183-211

  9. A solution relying on the model checking of boolean transition systems

    • Jorge Cuéllar, Dieter Barnard, Martin Huber
    Pages 213-251

  10. Applying a temporal logic to the RPC-memory specification problem

    • Reinhard Gotzhein
    Pages 253-273

  11. Using PVS for an assertional verification of the RPC-memory specification problem

    • Jozef Hooman
    Pages 275-304

  12. Specification and verification using a visual formalism on top of temporal logic

    • Hardi Hungar
    Pages 305-339

  13. A case study in verification based on trace abstractions

    • Nils Klarlund, Mogens Nielsen, Kim Sunesen
    Pages 341-373

  14. Incremental specification with joint actions: The RPC-memory specification problem

    • Reino Kurki-Suonio
    Pages 375-404

  15. The methodology of modal constraints

    • Kim G. Larsen, Bernhard Steffen, Carsten Weise
    Pages 405-435

  16. Tackling the RPC-memory specification problem with I/O automata

    • Judi Romijn
    Pages 437-475

  17. Using relations on streams to solve the RPC-memory specification problem

    • Ketil Stølen
    Pages 477-520

  18. The RPC-memory specification problem: UNITY + refinement calculus

    • Rob T. Udink, Joost N. Kok
    Pages 521-540

  19. Back Matter

    Download chapter PDF
Back to top

Keywords

About this book

The RPC-memory specification problem was proposed by Broy and Lamport as a case study in the formal design of distributed and concurrent systems. As a realistic example typical for operating systems and hardware design, the RPC-memory problem was used as the basis for comparing various approaches to formal specification, refinement, and verification.
Preliminary solutions were discussed during a workshop at Schloss Dagstuhl, Germany, in September 1994. Then an extensive discussion took place between the referees and authors. Finally 15 thoroughly revised papers were accepted for inclusion in this volume in full detail together with the problem statement and a synopsis.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation