P.: Formalization of Invariant Patterns for the Invariant Refinement Method

Abstract. Refining high-level system invariants into lower-level soft-ware obligations has been successfully employed in the design of ensemble-based systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathemati-cal 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 abstrac-tion and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns