The Library
A temporal logic for the specification and verification of real-time systems
Tools
Naik, Yogesh (1993) A temporal logic for the specification and verification of real-time systems. PhD thesis, University of Warwick.
|
PDF
WRAP_Theses_Naik_1993.pdf - Unspecified Version - Requires a PDF viewer. Download (6Mb) | Preview |
Official URL: http://webcat.warwick.ac.uk/record=b1416064~S15
Abstract
The development of a product typically starts with the specification of the user’s requirements and ends with the design of a system to meet those requirements. Traditional approaches to the specification and analysis of a system abstracted away from any notion of time at the specification level. However, for a real-time system the specification may include timing requirements. Many specification and verification methods for real-time systems are based on the assumption that time is discrete because the verification methods using it are significantly simpler than those using continuous time. Yet real-time systems operate in ‘real’ continuous time and their requirements are often specified using a continuous time model.
In this thesis we develop a temporal logic and proof methods for the specification and verification of a real-time system which can be applied irrespective of whether time is discrete, continuous or dense. The logic is based on the definition of the next operator as the next time point a change in state occurs or if no state change occurs then it is the time point obtained by incrementing the current time by one. We show that this definition of the next operator leads to a logic which is expressive enough for specifying real-time systems where continuous time is required, and in which the verification and proof methods developed for discrete time can be used. To demonstrate the applicability of the logic several varied examples including communication protocols and digital circuits are specified and their real-time properties proved. A compositional proof system which supports hierarchical development of programs is also developed for a real-time extension of a CSP-like language.
Item Type: | Thesis (PhD) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Library of Congress Subject Headings (LCSH): | Real-time data processing , Logic, Symbolic and mathematical, Temporal databases, Computer programs -- Verification, Semantics | ||||
Official Date: | March 1993 | ||||
Dates: |
|
||||
Institution: | University of Warwick | ||||
Theses Department: | Department of Computer Science | ||||
Thesis Type: | PhD | ||||
Publication Status: | Unpublished | ||||
Supervisor(s)/Advisor: | Joseph, M. | ||||
Extent: | v, 178 leaves | ||||
Language: | eng |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year