Regresar

Formalization of invariant patterns for the invariant refinement method

Abstract:

Refining high-level system invariants into lower-level software obligations has been successfully employed in the design of ensemblebased systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathematical analysis. This paper provides such a formalization and demonstrates it in the context of the Invariant Refinement Method. The formalization is used to formally define invariant patterns at different levels of abstraction and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns.