Naik, Yogesh (1993) A temporal logic for the specification and verification of real-time systems. PhD thesis, University of Warwick.

Preview

PDF WRAP_Theses_Naik_1993.pdf - Unspecified Version - Requires a PDF viewer. Download (6Mb) | Preview

Request Changes to record.

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 specifica­tion 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 defini­tion 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:	Date Event March 1993 Submitted
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