Specification - lgwagner/SpeAR GitHub Wiki

The specification is the main element used to describe an element and how it is to behave. SpeAR specifications go beyond typical requirements descriptions in that they include required behaviors, but also capture information the element will monitor (inputs to the element), information the element will compute (outputs of the element), and explicit assumptions that the element requires of the environment it operates within.

Each SpeAR specification contains the following sections. The Inputs, Outputs, and Requirements section are mandatory, while the other sections are optional and provided for convenience to the user. The following pages provide more information on the function of each section of the specification and how to correctly define elements contained within them.

Example

The following example shows a simple specification. First notice that specification begins with the Specification keyword and a name that uniquely identifies it. In this case the name is example1. Notice the specification has one input a and one output y. It also contains a single requirement r0 that specifies that the output is equal to the input incremented by 1. Finally, there is a property p0 that checks that the output is greater than the input.

Property p0 is trivially true. Obviously, if the output y is one greater than the input x, then it also greater than x. However, this arrangement represents something that is useful in requirements specifications. A higher-level requirement (p0) that is refined by a lower-level requirement (r0). This notion is useful for decomposing more abstract requirements into more concrete elements. SpeAR allows users to use model checking to verify this has been done correctly.

⚠️ **GitHub.com Fallback** ⚠️