{"id":{"repo_id":"rgu","oai_identifier":"oai:rgu-repository.worktribe.com:2807451"},"canonical_url":"https://search.dev.ndltd.org/etd/rgu/oai:rgu-repository.worktribe.com:2807451","repository":{"repo_id":"rgu","name":"Robert Gordon University","base_url":"https://rgu-repository.worktribe.com/oaiprovider"},"display":{"title":"A formal description language for specifying and verifying real-time software systems.","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Li, Junhai"],"institution":"Robert Gordon University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["D. Davidson and T. Miller"],"committee_chairs":[],"committee_members":[],"year":1994,"date_issued":"1994","date_published":"1994","updated_at":"2026-07-24T04:10:12Z","subjects":["Reliability description language(RDL)","Real-time software systems","Temporal logic","Stepwise refinement","Predefined templates","Decision procedure validation"],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["oai:rgu-repository.worktribe.com:2807451","https://doi.org/10.48526/rgu-wt-2807451"],"render_values":[{"text":"oai:rgu-repository.worktribe.com:2807451","href":null,"code":true},{"text":"https://doi.org/10.48526/rgu-wt-2807451","href":"https://doi.org/10.48526/rgu-wt-2807451","code":true}]}]},"links":{"outbound_url":"https://rgu-repository.worktribe.com/2807451/1/LI%201994%20A%20formal%20description%20language","outbound_label":"Repository record","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["D. Davidson and T. Miller"]},{"key":"dc:contributor.sponsor","label":"Sponsor","values":["RGU Internal Funding"]},{"key":"dc:creator","label":"Author","values":["Li, Junhai"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["1994-01-31"]},{"key":"dc:date.issued","label":"Date","values":["1994"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["Robert Gordon University"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://rgu-repository.worktribe.com/output/2807451"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Reliability description language(RDL)","Real-time software systems","Temporal logic","Stepwise refinement","Predefined templates","Decision procedure validation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["oai:rgu-repository.worktribe.com:2807451","https://doi.org/10.48526/rgu-wt-2807451"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://rgu-repository.worktribe.com/2807451/1/LI%201994%20A%20formal%20description%20language"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["A formal description language for specifying and verifying real-time software systems."]}]}],"canonical_facts":{"dc:contributor.advisor":["D. Davidson and T. Miller"],"dc:contributor.sponsor":["RGU Internal Funding"],"dc:creator":["Li, Junhai"],"dc:date":["1994-01-31"],"dc:date.issued":["1994"],"dc:description.abstract":["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."],"dc:identifier":["oai:rgu-repository.worktribe.com:2807451","https://doi.org/10.48526/rgu-wt-2807451"],"dc:identifier.uri":["https://rgu-repository.worktribe.com/2807451/1/LI%201994%20A%20formal%20description%20language"],"dc:language":["en"],"dc:publisher.institution":["Robert Gordon University"],"dc:relation.isreferencedby":["https://rgu-repository.worktribe.com/output/2807451"],"dc:subject":["Reliability description language(RDL)","Real-time software systems","Temporal logic","Stepwise refinement","Predefined templates","Decision procedure validation"],"dc:title":["A formal description language for specifying and verifying real-time software systems."],"dc:type":["Thesis"]},"updated_at":"2026-07-24T04:10:12Z"}