The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We present a complete solution to the Broy-Lamport specification problem. Our specifications are written in TLA+, a formal language based on TLA. We give the high levels of structured proofs and sketch the lower levels, which will appear in full elsewhere.
This paper describes a solution of the RPC-memory specification problem defined by M. Broy and L. Lamport on the occasion of a Dagstuhl seminar in 1994. The approach is based on a recently developed model of composable high-level Petri nets called M-nets, on which CCS-like composition operations such as parallel composition, restriction and transition synchronisation are defined. Correctness proofs...
We present a partial solution to the Dagstuhl RPC-Memory Specification Problem which is carried out in linear-time temporal logic (LTL). Our language is quite similar to TLA (Temporal Logic of Actions) by Lamport. However, our use of this language provides some (in our opinion) interesting novelties. A major contribution of this paper is in our opinion a demonstration of different structuring mechanisms...
We give a functional specification of the syntactic interface and the black box behavior of an unreliable and a reliable memory component and a remote procedure (RPC) call component. The RPC component controls the access to the memory. In addition, we specify a clerk for driving the RPC component. The used method is modular and therefore it allows us to specify each of these components independently...
In this paper we present the Temporal Language of Transitions (TLT) solution to the RPC Memory Specification Problem posed by Lamport for a Dagstuhl seminar. TLT is a framework for the compositional specification and verification of distributed systems. In our solution we show how the TLT specifications can be factorized to extract their finite-state control parts. This leads to straightforward refinement...
The unreliable and the reliable memory component of the RPC-Memory Specification Problem are specified and verified using a formalism that is based on a temporal logic. In that formalism, a system (open and/or distributed) consists of the system architecture and the system behaviour. The architecture is specified by defining the sets of its agents (=active components) and interaction points (= conceptual...
The RPC-Memory Specification Problem has been specified and verified in an assertional method, supported by the verification system PVS. Properties of the components are expressed in the higher-order logic of PVS and all implementations have been verified by means of the interactive proof checker of PVS. A simplification of the memory specification — allowing multiple atomic reads — has been proved...
The problem is treated with a method whose main concern is the formal verification of key properties of a design. Availability of largely automatic verification procedures is, for this purpose, considered the most important point, less emphasis is put on completeness of the specification. Another distinguishing characteristic of this solution is the rôle of the remote procedure call protocol. Any...
In [14], we proposed a framework for the automatic verification of reactive systems. Our main tool is a decision procedure, Mona, for Monadic Second-order Logic (M2L) on finite strings. Mona translates a formula in M2L into a finite-state automaton. We show in [14] how traces, i.e. finite executions, and their abstractions can be described behaviorally. These state-less descriptions can be formulated...
Solutions to the RPC-Memory Specification Problem are developed incrementally, using an object-oriented modeling formalism with multi-object actions. Incrementality is achieved by superposition-based derivation steps that make effective use of multiple inheritance and specialization of inherited actions. Each stage models collective behaviors of objects at some level of abstraction, and the preservation...
We present a complete solution of the RPC-Memory Specification Problem, by applying a constraint-oriented state-based proof methodology for concurrent software systems. Our methodolgy exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which...
An I/O automata solution to the problem posed in 1994 by Broy & Lamport at the Dagstuhl Workshop on Reactive Systems is presented. The problem calls for specification and verification of memory and remote procedure call components. The problem specification consists of an untimed and a timed part. In this paper, both parts are solved completely.
We employ a specification and refinement technique based on streams to solve the RPC-memory specification problem. Streams are used to represent the communication histories of channels. We distinguish between input and output streams. Each input stream represents the communication history of an input channel; each output stream represents the communication history of an output channel. Specifications...
We use the ImpUNITY framework to solve the “RPC-Memory Specification problem” of the Dagstuhl Workshop on reactive systems. ImpUNITY supports the development of parallel and distributed programs from specification to implementation in a stepwise manner. It is an extension of UNITY, as introduced by Chandy and Misra, with features of the Action System formalism of Back and Kurki-Suonio. Due to this...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.