Refinement-based reasoning of optimized reactive systems
Mitesh Jain · 2018
We show that the correctness of a large class of optimized reactive systems can be effectively analyzed using refinement. Reasoning about reactive systems using refinement involves showing that any (infinite) behavior of a low-level, concrete implementation system is a behavior of the high-level abstract specification system. Existing notions of refinement do directly account for the differences in the unobservable behaviors (stuttering) of a concrete implementation and its abstract specification. However, they do not directly account for the differences in the observable behaviors of an optimized implementation and its abstract specification. Towards this we introduce two new notions of correctness, skipping simulation and reconciling simulation and develop a theory of refinement based on it. We study their algebraic properties and present several sound and complete proof-methods that can be used to effectively reason about them. The proof-methods reduce global reasoning about infinite computations of reactive systems to local reasoning about states and their successors and therefore are amenable to mechanical reasoning using existing verification tools--Author's abstract