Realizability - lgwagner/SpeAR GitHub Wiki

Realizability analysis seeks to prove that the given specification is conflict free for all possible inputs. This is a more rigorous analysis than the Logical Consistency check. Logical Consistency attempts to prove that no trace exists of length N which satisfies all of the assumptions and requirements. This analysis attempts to prove that every possible trace in the system is free of conflict. Realizability is able to prove that a system is free of conflict whereas Logical Consistency is simply a bug-finding tool.

This example shows a simple specification that takes one input, a and returns one output b. It has two requirements, r0 and r1 which are clearly in conflict. Requirement r0 requires that a == 3 implies b == 2, and r1 requires that if a == 3 implies b == 3. Logical consistency analysis is able to identify at least one trace that satisfies this model. Any trace in which a is not equal to 3 satisfies it. However, there is a conflict when a == 3. Realizability analysis will identify this error.

The underlying realizability tool, jRealizability, is a prototype. It can return a result of unknown, and often will for large models.