<%@ 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-197

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

A. Goswami, M. Bell and M. Joseph, ISL: An Interval Logic for the Specification of Real-time Programs (October 1, 1991).

Abstract

ISL is a linear-time temporal logic for specifying properties of programs in execution intervals which are sequences of states. The end points of intervals are specified using instances of state predicates (or assertions) or time values. Abstract intervals, delimited by formulae over states in a computation, are used as the first step in constructing a timed specification. This is then transformed to incorporate timing, first by logical formulae and then using concrete time domains. Refinements are introduced to define time domains and timing properties and include refinement to programming constructs. We outline a way to specify resource limitations along with the functional and timing properties of programs. The specification method is illustrated with some examples. To be presented at the Symposium on Real-time and Fault-tolerant Systems, Nijmegen, The Netherlands, 8-10 January 1992.

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

A. Goswami, M. Bell and M. Joseph, "ISL: An Interval Logic for the Specification of Real-time Programs", Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 571, ed. J. Vytopil, Springer-Verlag, pp. 1-20 (1991)

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