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.

翻译：信息物理系统因其软件与物理世界的关联而具有内在复杂性。迭代设计可降低其复杂性，但每次修改后需完整重新验证安全性的需求随之增加。我们提出"重构即命题"原则，将重构表示为命题，并通过沿相应修改传递证明的方法，验证系统重构能保持其必要属性。该方法基于微分精化逻辑(dRL)，可同时严谨地指称系统属性及重构系统与原版本间的关系。精化提供了一种统一表达不同类型混成系统重构的方式，包括引入辅助变量的重构。此外，我们展示了如何自动验证这些重构，以及如何将其归约为仅关注局部变更的模块化证明，而非整个系统的验证。