<%@ page language="java" contentType="text/html" %> <%-- Include common initialisation code --%> <%@ include file="/arch/common.jsp" %> <%-- The current tab --%> <% String currentTab = "Research"; %> <%-- Content of navigation pane --%> <%@ include file="nav.jsp" %> <% showCurrentLink=true; %> <%-- Current navigation location --%> <% String currentNav = "Reports and Theses"; %> <%-- Include the code for the document header --%> <%@ include file="/arch/header.jsp" %>

Research Report CS-RR-259

<%-- Include the code for the lines and navigation --%> <%@ include file="/arch/middle.jsp" %>

Yogesh Naik, A Temporal Logic for the Specification and Verification of Real-Time Systems (March 1, 1994).

Abstract

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.

<%@ include file="hardcopy.html" %>

There is a charge of £8.00 for this document to cover our costs.

<%-- Include the code for the document footer --%> <%@ include file="/arch/footer.jsp" %>