% ============================================================================= PatternPool BuildAutLightControl 0: OrganizationalAspects: ProjectName: ??? Authors: Peper, Kronenburg, Gotzhein Status: % ============================================================================= PatternDefinitions: Pattern Invariance (p) Intention : Allows to specify that a certain property must always hold. Example : \always tempActGtZero tempActGtZero is always valid. Definition : \always p p is always valid. Properties : Comment : % ============================================================================= Pattern ConditionalBoundedResponse (p, q, t) Intention : Allows to express that a property (the response) becomes true within a given time if another property (the condition) is valid during the whole time. Example : \always ((hazardousCondition \and \not windowClosed) \impl \eventually_{\le 30 s} [windowClosed \or \not hazardousCondition]) Whenever a hazardous condition is detected, but the window is not closed, then the window will be closed within 30 seconds, or the hazardous condition ceases within this time interval. Definition : \always ((p \and \not q) \impl \eventually_{\le t} [q \or \not p]) Whenever p is true, but q is false, then q becomes also true within t time units, or p ceases within this time interval. Properties : Comment : % ============================================================================= Pattern ConditionalContinuity (p, q) Intention : Allows to express that a property is true at least as long as another property (the condition) is true. Example : \always ((hazardousCondition \and windowClosed) \impl (windowClosed \waitsfor \not hazardousCondition)) Whenever a hazardous condition is detected and the window is closed, then the window will remain closed at least as long as the hazardous condition is true. Definition : \always ((p \and q) \impl (q \waitsfor \not p)) Whenever p and q are both true, then q remains true at least as long as p is true. Properties : Comment : % ============================================================================= Pattern ConditionalBoundedResponseAndContinuity (p, q, t) Intention : This pattern is a combination of the two patterns ConditionalBoundedResponse and ConditionalContinuity. Example : \always (hazardousCondition \impl \eventually_{\le 30 s} ((windowClosed \and (windowClosed \waitsfor \not hazardousCondition)) \or \not hazardousCondition)) Whenever a hazardous condition is detected, then, within 30 s, the window is closed and will stay closed at least as long as the hazardous condition is true, or the hazardous condition releases. Definition : \always (p \impl \eventually_{\le t} ((q \and (q \waitsfor \not p)) \or \not p)) Whenever j is true, then, within t time units, y becomes also true and stays true at least as long as j, or j releases. Properties : Comment : See the comment of the pattern DelayedImplication. % ============================================================================= Pattern DelayedImplication (p, q, t) Intention : q is depending on p with a maximal time delay t. Example : \always (hazardousCondition \delImpl_{\le 30 s} windowClosed) Whenever a hazardous condition holds continuously for at least 30 s, then eventually within this time span, the window is closed and remains closed at least as long as the hazardous condition continues. Definition : \always (p \delImpl_{\le t} q) Whenever j holds continuously for at least t time units, then eventually within this time span, y is true and remains true at least as long as j. Properties : \always (p1 \delImpl_{\le t1} p2) \and \always (p2 \delImpl_{\le t2} p3) \impl \always (p1 \delImpl_{\le t1+t2} p3) \always (p \delImpl_{\le t} q1) \and \always (p \delImpl_{\le t} q2) \impl \always (p \delImpl_{\le t} (q1 \and q2)) Comment : This pattern is very similar to the pattern ConditionalBoundedResponseAndContinuity. The differences are that the delayed implication pattern allows a "fluttering" of the value of q during the time t which is not possible for the pattern ConditionalBoundedResponseAndContinuity. % ============================================================================= Pattern DelayedEquivalence (p, q, t) Intention : The truth value of q is a time displaced copy of the truth value of p. Example : \always (hazardousCondition \and windowOpen \delEquiv_{\le 30 s} warnedUser) Supposed, the window is only manually operable. Whenever the window is continuously open during a hazard ous condition for at least 30s, then eventually within this time span, the user is warned and remains warned at least as long as the precondition is true. And conversely, whenever there is a closed window or no hazardous condition for at least 30 s, then eventually within this time span, the user warning is suppressed and remains suppressed at least as long as this precondition holds. Definition : \always (p \delEquiv_{\le t} q) Properties : Comment : % ============================================================================= Pattern LimitedInvariance (p, t) Intention : Suppression of the "fluttering" of a property, i.e. the fast change of the value of the property. In a certain sense, this pattern is a kind of low pass filter enabling only slow state changes. Allows to express that a property that is acchieved remains unchanged for a certain time. Example : \always ( \[windowOpen\] \impl \always_{\le 5 min} windowOpen ) Each time the window is open, it will stay open for at least 5 minutes. If a lower bound for the close time is given in the same manner, the frequency for window state changes is limited by 1/(2x5 min) = 1.67x10^{-3} Hz. Definition : \always ( \[p\] \impl \always_{\le t} p ) Each time j becomes true, it will stay true for at least t time units. Properties : \always ( \[p \and q\] \impl \always_{\le t} p \and q) \impl \always ((\[p\] \impl \always_{\le t} p}) \or (\[q\] \impl \always_{\le t} q})) \always ((\[p\] \impl \always_{\le t} p}) \or (\[q\] \impl \always_{\le t} q})) \impl \always ( \[p \or q\] \impl \always_{\le t} p \or q) Comment : % ============================================================================= Pattern AccumulatedInvariance (p, T, t) Intention : The system must satisfy a property p at least for a certain time, but the exact points of times are unimportant. Note, that the time t could also be replaced by a ratio t/T to allow a percental specification. Example : \always \accInv^{1 h}_{\ge 12 min} windowOpen Within any hour the window is open for at least 12 minutes. I.e., the window is open 20% of the total time to enable sufficient ventilation. Definition : \always \accInv^{T}_{\ge t} p Within any time interval T, p is true for at least t time units. Properties : Comment : % =============================================================================