A Supermodel Framework Supporting Validated Upgrading of Reactive Systems

摘要

A software product is typically “upgraded” many times over its lifetime. Reactive systems are no exception, undergoing evolutionary version changes to add features and fix bugs. Evolving these stateful systems, such as email clients, software agents, smart cell phones, and personal digital assistants, is complicated 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 automated reasoning techniques like theorem proving or 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. It then presents a simple and widely applicable upgrade framework, based upon the idea of a supermodel that allows upgrade behavior to be validated using mainstream approaches. Finally, it also gives techniques for simplifying the validation problem.