A formal description language for specifying and verifying real-time software systems.

This thesis describes a study of the reliability description language(RDL) as a formal language for specifying concurrent/real time systems and temporal logic as a basis for developing the semantics of the language. It also presents a stepwise refinement approach, a preprocessor and a library of templates which support the use of RDL in the specification of relatively complex systems. RDL is used to specify solutions to a number of realistic problems. The systems specified range over critical region, producer and consumer, dining philosophers problems as well as the alternating bit protocol and the sliding window protocol. The liveness and safety properties of these systems are formulated in terms of temporal logic. The stepwise refinement approach can be used to develop hierarchical specifications of individual RDL components. An RDL component of a specification can be selected and refined into a more detailed description. Consistency refinement rules are defined in terms of temporal logic. The rules ensure that lower levels correctly refine upper levels of a specification. The conditions for checking consistency between a ‘high-level’ and its direct refinement are constructed automatically using the refinement approach. The conditions can be validated using an existing decision procedure. The preprocessor can be used to compose an overall system starting from a single module leading to a tree-like structure with leaf nodes containing fully refined description of all RDL components. A library containing predefined templates is proposed for achieving reusable RDL specifications. Fully parameterised specification is possible with the proposed library. Specification generators can be constructed using the reusable templates in the library.

Grantor dc:publisher.institution

Robert Gordon University

Year dc:date.issued

1994

Author dc:creator

• Li, Junhai

Advisor dc:contributor.advisor

• D. Davidson and T. Miller

• Reliability description language(RDL)
• Real-time software systems
• Temporal logic
• Stepwise refinement
• Predefined templates
• Decision procedure validation

Language dc:language

en

Identifier

oai:rgu-repository.worktribe.com:2807451
https://doi.org/10.48526/rgu-wt-2807451

OAI identifier oai:identifier

oai:rgu-repository.worktribe.com:2807451