Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

A temporal logic for the specification and verification of real-time systems

Tools
- Tools
+ Tools

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

[img]
Preview
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

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 or Dissertation (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:
DateEvent
March 1993Submitted
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 View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us