A Framework for Flexible Program Evolution and Verification of Distributed Systems

Abstract

Program evolution may reveal bad design decisions, misunderstandings, erroneous code, or erroneous specifications, because problems made early in the design of a system may not be discovered until much later in the life-time of the system. Non-trivial changes of old code may be necessary. Flexibility in making such changes is essential, especially in a distributed setting where the system components are updated independently. In this setting re-verification is challenging. We consider flexibility with respect to what changes can be made as well as what can be efficiently reverified. In this paper we propose a flexible framework for modeling and evolution of distributed systems. It supports unrestricted modifications in such systems, both in code and specifications, and with support of verification and re-verification. We consider on the setting of concurrent and object-oriented distributed programs, and introduce a core high-level modeling language supporting active objects. We allow multiple inheritance because it gives added flexibility during evolution, allowing a wider class of software changes. To avoid undesired effects of multiple inheritance, we apply a healthy binding strategy. We prove that the framework supports Modification Independence and Hierarchy Independence, which requires healthy binding. We demonstrate that our framework can deal with verification of software changes that are not possible in comparable frameworks.