ISL - AN INTERVAL LOGIC FOR THE SPECIFICATION OF REAL-TIME PROGRAMS
UNSPECIFIED. (1991) ISL - AN INTERVAL LOGIC FOR THE SPECIFICATION OF REAL-TIME PROGRAMS. LECTURE NOTES IN COMPUTER SCIENCE, 571 . pp. 1-20. ISSN 0302-9743Full text not available from this repository.
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.
|Item Type:||Journal Article|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Journal or Publication Title:||LECTURE NOTES IN COMPUTER SCIENCE|
|Number of Pages:||20|
|Page Range:||pp. 1-20|
Actions (login required)