Skip to content

Response Invariance Property Pattern

Jump to bottom
Marc Carwehl edited this page Dec 16, 2021 · 4 revisions

Description

State-Based Pattern

Untimed

Globally

This scope is equivalent to 'Universality, After Q' where Q is P and the original P is S.

Before R

A[] not ERROR

Response Invariance before R untimed observer

After Q

A[] not ERROR

Response Invariance after Q untimed observer

Between Q and R

A[] not ERROR

Response Invariance between Q and R untimed observer

After Q Until R

A[] not ERROR

Response Invariance after Q until R untimed observer

Timed

  • u specifies the upper time bound, l specifies the lower time bound

Globally

A[] (waiting AND l < c AND c < u) imply S

Response Invariance state globally timed

Before R

A[] not ERROR

Response Invariance before Q timed observer

After Q

A[] not ERROR

Response Invariance after R timed observer

Between Q and R

A[] not ERROR

Response Invariance between Q and R timed observer

After Q Until R

A[] not ERROR

Response Invariance after Q until R timed observer

Home

Specification Pattern Catalogue for UPPAAL

Evaluation

Clone this wiki locally