Formalizing correctness criteria of dynamic updates derived from specification changes

Modern software-intensive systems often have to be updated to adapt to unpredicted changes in their environments or to satisfy unpredicted requirement changes. Many systems, however, cannot be easily shut down or are expected to run continuously. Therefore, they must be updated dynamically, at run-time. Especially for critical systems, dynamic updates must be safe and performed as soon as possible. We recently studied the relationship between specification changes and dynamic updates and defined a criterion for when a system can safely disregard its current obligations and how it should change its behavior to satisfy the new specification. In this paper, we study further examples that show that stronger and weaker variants of our original criterion are relevant when engineering dynamically updating software. We formalize these criteria and discuss their safety. Moreover, we provide a tool for synthesizing dynamically updating controllers from changes in scenario-based specifications that respect the new criteria.