PIL--- An Temporal Logic for Real-Time Requirements in Embedded Systems

摘要

The precise and understandable description of temporal requirements is of increasing importance in the development of embedded systems. In colloquial speech, it is very common to state temporal properties by using time points to denote starting or end points of a given property. On the other hand intervals are appropriate, for example, for the description of a desired duration of a property. To gain a logic that combines the advantages of interval logic and the possibility to denote margins of an interval we introduce the Point Interval Logic (PIL). PIL is an interval logic based on the Duration Calculus (DC) that extend its applicability. The DC was introduced in reference 1 and extended in reference 14 as a notation to specify hybrid and real-time systems. Thus PIL inherits the capabilities of the DC for example to use differential equations to specify hybrid systems. Apart from that, PIL is designed with a special emphasis on the appearance of the formulas. The DC is extended to obtain an easy to use notation to specify temporal properties.