Logical Entailment - lgwagner/SpeAR GitHub Wiki
Logical entailment is an analysis that shows that the assumptions and requirements of a SpeAR specification logically imply each property of the specification. SpeAR is a constraint-based specification framework. This means that prior to expressing assumptions and requirements, the specification allows any possible relationship to hold between the inputs and outputs. Each requirement and assumption then defines a relation between the inputs and outputs, which constraints the possible behaviors the system allows. When a specification is complete, logical entailment can be used to show that the system, as it is constrained by assumptions and requirements, allows (or forbids) certain desirable (or undesirable) behaviors to occur. This can be invaluable for validating that the assumptions and requirements accurately and precisely describe the element under development.
Logical entailment analysis also supports the identification of traces that observe a desired behavior. This is accomplished by adding the "observe" keyword on any property between the name and the ":" keyword. The tool will look for a trace that satisfies the property expression. This can be used as a test or a way to confirm that your model behaves as intended. Finally, Logical entailment analysis also supports Traceability, when the IVC option is enabled through the Configuration of SpeAR Preferences page.
The accompanying image shows a partial specification that has three Boolean inputs (a,b,c) and two Boolean outputs (x,y). This specification is partial because it defines x as true when a or b is true (but defines no behavior when a and b are both false) and defines y as true when a and b are true or when c is true (but defines no behavior when a and b is not true or c is false). The property p0 is found to be true because r0 and r1 explicitly identify that x and y are both true when a and b are both true. Property observe_p0 finds a trace that observes property p0. Property p1 is false because while c implies y, the opposite does not hold. y is also true when a and b are true, but it could also be true when a and b is false, or c is false, because the behavior in that case is not specified. SpeAR will allow y to take on any value it wants in that instance.
It is possible to define partial specifications (a specification for which behaviors are defined for some input/output combinations) and conflicting specifications (a specification for which two or more different behaviors are specified for a given input/output combination) in SpeAR. Logical entailment analysis is not concerned with whether the specification is partial or in conflict. Instead, logical entailment seeks to demonstrate that the combination of assumptions and requirements logically entail (imply) each property in the specification. Partial specifications may satisfy its given properties (given that the properties expressed only cover the behaviors covered by the assumptions and requirements) or they may provide spurious violations (if the property is concerned with an unspecified portion of the specification). In addition, conflicting specifications **always** satisfy its properties due to the way the analysis is encoded in the underlying Lustre representation.
In the former scenario, the user will have to rely on their understanding of the model to understand that their property covers an unspecified portion of the specification. This may or may not be evident in the counterexample provided by the tool. In the latter scenario it is important for the user to also rely on the other analyses Logical Consistency and Realizability to ensure there are not conflicts in their specifications.