{"id":{"repo_id":"texas","oai_identifier":"oai:repositories.lib.utexas.edu:2152/63185"},"canonical_url":"https://search.dev.ndltd.org/etd/texas/oai:repositories.lib.utexas.edu:2152/63185","repository":{"repo_id":"texas","name":"University of Texas","base_url":"https://repositories.lib.utexas.edu/server/oai/request"},"display":{"title":"Specification and analysis of timing properties in real-time systems","abstract":"This dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute timing of events. Relative timing concerns the order in which events occur, such as mutual exclusion and precedence constraint properties. Absolute timing concerns the stringent timing restrictions imposed on a system, such as a response time deadline or a minimum elapsed time between occurrences of two events. The approach is based on Real Time Logic (RTL), a logic invented primarily for the specification of both relative and absolute timing of events. The notion of an event occurrence is central to RTL; an event occurrence marks a point in time which is of significance to the behavior of a system. Hence, concurrency is modeled as a partial ordering of the event occurrences in the system. A system specification and a property to be verified can be expressed as arithmetical relations on algebraic expressions involving the event occurrences. To verify the property with respect to the system specification, we prove that the property is a theorem derivable from the specification. Relationship of RTL to Presburger Arithmetic is discussed and a verification technique based on inequality provers is explored. The dissertation also introduces a specification language, Modechart, for real-time systems. The semantics of Modechart is described in terms of RTL formulas. In Modechart, we make use of the concept of modes which can be thought of as partitioning the state space of a system. Intuitively, modes can be viewed as control information that impose structure on the operation of a system. Modes are arranged hierarchically. Furthermore, modes at the same level of hierarchy can be related in one of two ways: in series or in parallel. A transition can be specified between two modes in series, but no transition is allowed between modes in parallel. The language allows sporadic/periodic actions in modes as well as constructs for specifying timing constraints such as delays and deadlines on mode transitions. Verification procedures are introduced for showing a Modechart specification satisfies a property expressed as an RTL formula.","abstract_html":"This dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute timing of events. Relative timing concerns the order in which events occur, such as mutual exclusion and precedence constraint properties. Absolute timing concerns the stringent timing restrictions imposed on a system, such as a response time deadline or a minimum elapsed time between occurrences of two events. The approach is based on Real Time Logic (RTL), a logic invented primarily for the specification of both relative and absolute timing of events. The notion of an event occurrence is central to RTL; an event occurrence marks a point in time which is of significance to the behavior of a system. Hence, concurrency is modeled as a partial ordering of the event occurrences in the system. A system specification and a property to be verified can be expressed as arithmetical relations on algebraic expressions involving the event occurrences. To verify the property with respect to the system specification, we prove that the property is a theorem derivable from the specification. Relationship of RTL to Presburger Arithmetic is discussed and a verification technique based on inequality provers is explored. The dissertation also introduces a specification language, Modechart, for real-time systems. The semantics of Modechart is described in terms of RTL formulas. In Modechart, we make use of the concept of modes which can be thought of as partitioning the state space of a system. Intuitively, modes can be viewed as control information that impose structure on the operation of a system. Modes are arranged hierarchically. Furthermore, modes at the same level of hierarchy can be related in one of two ways: in series or in parallel. A transition can be specified between two modes in series, but no transition is allowed between modes in parallel. The language allows sporadic/periodic actions in modes as well as constructs for specifying timing constraints such as delays and deadlines on mode transitions. Verification procedures are introduced for showing a Modechart specification satisfies a property expressed as an RTL formula.","abstract_has_math":false,"creators":["Jahanian, Farnam"],"institution":"University of Texas at Austin","degree_name":"Doctor of Philosophy","degree_level":"Doctoral","degree_discipline":"Computer Sciences","degree_department":null,"school":null,"contributors":[],"advisors":["Mok, Aloysius Ka-Lau"],"committee_chairs":[],"committee_members":[],"year":1988,"date_issued":"1988","date_published":"1988","updated_at":"2026-07-24T05:01:20Z","subjects":[],"languages":["eng"],"rights":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["doi:10.15781/T2H12VQ50"],"render_values":[{"text":"doi:10.15781/T2H12VQ50","href":"https://doi.org/10.15781/T2H12VQ50","code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2152/63185","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Mok, Aloysius Ka-Lau"]},{"key":"dc:creator","label":"Author","values":["Jahanian, Farnam"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2018-01-24T16:12:08Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2018-01-24T16:12:08Z"]},{"key":"dc:date.issued","label":"Date","values":["1988"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Sciences"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Doctoral"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Texas at Austin"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["doi:10.15781/T2H12VQ50"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/2152/63185"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["This dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute timing of events. Relative timing concerns the order in which events occur, such as mutual exclusion and precedence constraint properties. Absolute timing concerns the stringent timing restrictions imposed on a system, such as a response time deadline or a minimum elapsed time between occurrences of two events. The approach is based on Real Time Logic (RTL), a logic invented primarily for the specification of both relative and absolute timing of events. The notion of an event occurrence is central to RTL; an event occurrence marks a point in time which is of significance to the behavior of a system. Hence, concurrency is modeled as a partial ordering of the event occurrences in the system. A system specification and a property to be verified can be expressed as arithmetical relations on algebraic expressions involving the event occurrences. To verify the property with respect to the system specification, we prove that the property is a theorem derivable from the specification. Relationship of RTL to Presburger Arithmetic is discussed and a verification technique based on inequality provers is explored. The dissertation also introduces a specification language, Modechart, for real-time systems. The semantics of Modechart is described in terms of RTL formulas. In Modechart, we make use of the concept of modes which can be thought of as partitioning the state space of a system. Intuitively, modes can be viewed as control information that impose structure on the operation of a system. Modes are arranged hierarchically. Furthermore, modes at the same level of hierarchy can be related in one of two ways: in series or in parallel. A transition can be specified between two modes in series, but no transition is allowed between modes in parallel. The language allows sporadic/periodic actions in modes as well as constructs for specifying timing constraints such as delays and deadlines on mode transitions. Verification procedures are introduced for showing a Modechart specification satisfies a property expressed as an RTL formula."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["electronic"]},{"key":"dc:title","label":"Title","values":["Specification and analysis of timing properties in real-time systems"]}]}],"canonical_facts":{"dc:contributor.advisor":["Mok, Aloysius Ka-Lau"],"dc:creator":["Jahanian, Farnam"],"dc:date.accessioned":["2018-01-24T16:12:08Z"],"dc:date.available":["2018-01-24T16:12:08Z"],"dc:date.issued":["1988"],"dc:description.abstract":["This dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute timing of events. Relative timing concerns the order in which events occur, such as mutual exclusion and precedence constraint properties. Absolute timing concerns the stringent timing restrictions imposed on a system, such as a response time deadline or a minimum elapsed time between occurrences of two events. The approach is based on Real Time Logic (RTL), a logic invented primarily for the specification of both relative and absolute timing of events. The notion of an event occurrence is central to RTL; an event occurrence marks a point in time which is of significance to the behavior of a system. Hence, concurrency is modeled as a partial ordering of the event occurrences in the system. A system specification and a property to be verified can be expressed as arithmetical relations on algebraic expressions involving the event occurrences. To verify the property with respect to the system specification, we prove that the property is a theorem derivable from the specification. Relationship of RTL to Presburger Arithmetic is discussed and a verification technique based on inequality provers is explored. The dissertation also introduces a specification language, Modechart, for real-time systems. The semantics of Modechart is described in terms of RTL formulas. In Modechart, we make use of the concept of modes which can be thought of as partitioning the state space of a system. Intuitively, modes can be viewed as control information that impose structure on the operation of a system. Modes are arranged hierarchically. Furthermore, modes at the same level of hierarchy can be related in one of two ways: in series or in parallel. A transition can be specified between two modes in series, but no transition is allowed between modes in parallel. The language allows sporadic/periodic actions in modes as well as constructs for specifying timing constraints such as delays and deadlines on mode transitions. Verification procedures are introduced for showing a Modechart specification satisfies a property expressed as an RTL formula."],"dc:format.medium":["electronic"],"dc:identifier":["doi:10.15781/T2H12VQ50"],"dc:identifier.uri":["http://hdl.handle.net/2152/63185"],"dc:language.iso":["eng"],"dc:rights":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."],"dc:title":["Specification and analysis of timing properties in real-time systems"],"dc:type":["Thesis"],"thesis:degree_discipline":["Computer Sciences"],"thesis:degree_level":["Doctoral"],"thesis:degree_name":["Doctor of Philosophy"],"thesis:institution_name":["University of Texas at Austin"]},"updated_at":"2026-07-24T05:01:20Z"}