查看文章

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 …