Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements

TL;DR

This paper presents a formal method for rigorously verifying that system refactorings in cyber-physical systems preserve safety properties using differential refinement logic, enabling modular and automated proofs.

Contribution

It introduces the refactoring-as-propositions principle and a proof method based on differential refinement logic for verified hybrid system refactorings.

Findings

Refactorings can be represented as propositions with preserved properties.

Proofs can be transferred along system modifications to ensure safety.

Refactorings can be proved automatically or reduced to local proofs.

Abstract

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change. We introduce the refactoring-as-propositions principle in which refactorings are represented as propositions along with a method for proving that system refactorings preserve their required properties by transferring the proof along the respective modification. It is based on differential refinement logic (dRL), with which one can simultaneously and rigorously refer to properties of the systems and the relation between a refactored system and its original version. Refinements represent a uniform way of expressing different types of hybrid system refactorings, including those that introduce auxiliary variables. Furthermore, we show how these refactorings can be proved automatically, and/or reduce to a modular proof solely about the local change rather than about the whole system.