Real-Time System: Specification and Verification
Abstract
Temporal Interval Logic by virtue of its abstract interval constructors offers an excellent setting for concurrent system specification. Making extensions for this logic to cater to specification of quantitative aspects of behaviors was considered useful. Extensions have been made to for specifying real-time constraints in the framework of the logic. A formal semantics has been given. A large body of realistic and nontrivial examples have been explored and specified. The examples considered suggest that real-time variants of temporal interval logic are extremely suitable for quantitative specification of behaviors. The work was published at the 9th symposium on real- time systems, held in December 1988 at Huntsville, Alabama. A revision of the paper is currently under way so as to submit it for a journal. The work needs to be explored further in the direction of decision procedures for finite state real-time controllers. In an earlier work we proved that temporal interval logic is PSpace Complete. We have obtained decision procedures and implementations. We have synthesized using our implementation a hardware arbiter. This in itself is a substantial achievement for the synthesis times in our Prolog based implementation were quite reasonable. Thus the logic was demonstrated to be useful.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 28, 1989
- Accession Number
- ADA206467
Entities
People
- K. T. Narayana
Organizations
- Pennsylvania State University