Applying a Temporal Logic to the RPC-Memory Specification Problem

R. Gotzhein

in: M. Broy, S. Merz und K. Spies (Hrsg.): Formal Systems Specification - The RPC-Memory Specification Case Study, LNCS 1169, 1996, pp. 253-273

Zusammenfassung

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 locations of interactions), and by associating with each agent a set of interaction points. The behaviour is built from external actions and defined by the logical conjunction of all component behaviours. A component behaviour is specified by the conjunction of logical safety and liveness properties. For the memory component, a many­sorted first­order branching time temporal logic with operators to refer to the future, the past, actions, the number of actions, and intervals constructed in the (linear) past are used. It is proven that the reliable memory is a correct implementation of the unreliable memory. The proof obligation takes both the system architecture and the system behaviour into account. Finally, it is discussed whether architectural requirements should be formally expressed.

Vollversion




 Übergeordnete Seite: Jahr 1996

 Feedback
Zu den Kontaktdetails des Verantwortlichen dieser Seite

 English
This page in english. Diese Seite auf englisch.