Formal Systems Specification The RPC-Memory Specification Case Study
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...
| Other Authors: | , , |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
1996, 1996
|
| Edition: | 1st ed. 1996 |
| Series: | Lecture Notes in Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- The RPC-memory specification problem problem statement
- The RPC-memory case study: A synopsis
- A TLA solution to the RPC-memory specification problem
- A dynamic specification of the RPC-memory problem
- A memory module specification using composable high-level petri nets
- Constraint oriented temporal logic specification
- A functional solution to the RPC-memory specification problem
- A solution relying on the model checking of boolean transition systems
- Applying a temporal logic to the RPC-memory specification problem
- Using PVS for an assertional verification of the RPC-memory specification problem
- Specification and verification using a visual formalism on top of temporal logic
- A case study in verification based on trace abstractions
- Incremental specification with joint actions: The RPC-memory specification problem
- The methodology of modal constraints
- Tackling the RPC-memory specification problem with I/O automata
- Using relations on streams to solve the RPC-memory specification problem
- The RPC-memory specification problem: UNITY + refinement calculus