Upgrading legacy instances of reactive systems

A software product typically goes through many “upgrades” (version changes) over its lifetime. Reactive systems, such as e-mail clients, software agents, proxies, traffic controllers, and telephone switches are no exception. Evolving such stateful systems is made difficult by the fact that new versions of the software must deal correctly with legacy instances. Users of earlier versions have invested significant resources in creating the state of the legacy instance, and usually require that this state be upgraded appropriately when the new system version is activated. However, validating the correctness of this upgrading behavior is particularly difficult, whether through testing or more formal techniques like model checking, because legacy states are typically unreachable to the new version of the software. This paper explores this problem and requirements for its solution; presents a simple conceptual and modeling/programming upgrade framework, based upon the idea of a supermodel that allows upgrade behavior to be validated using mainstream approaches; and gives techniques for simplifying the validation problem