Logical Consistency - lgwagner/SpeAR GitHub Wiki

Logical Consistency analysis constructs a property that attempts to prove that no length N (configurable by the user) trace exists that satisfies all of the assumptions and requirements in a model. If the property is proven, then the user knows that a conflict exists within the requirements and assumptions that allow no traces to satisfy the set. In this scenario, the Logical Entailment analysis would prove all properties vacuously, giving the user unwarranted confidence that their specification is correct.

This example contains a simple specification that has one input x and one output y, both of type integer. Assumption a0 specifies that x is greater than 0. Requirement r0 specifies that y is less than 0, and requirement r1 specifies that y is greater than x. Clearly, among these three constraints, there is a conflict. The analysis result identifies this and also provides users the ability to determine which set of requirements are conflict. This can be done by right-clicking on the failed analysis and selecting "Show Conflicting Constraints" as shown in the associated image.

Logical Consistency analysis cannot prove that a given specification is consistent for all traces. Some specifications can satisfy the logical consistency check and still contain errors. It is important for users to realize that the logical consistency analysis is not a proof of logical consistency, but merely a tool to help identify errors in specifications. The Realizability analysis proves that a system is conflict-free for all traces, but it often returns a result of unknown for larger specifications and as a result, cannot always be relied upon.