Toward a Unified Operational Semantics-Based Approach to Modeling and Verifying Dynamic Software Updating

摘要

Internet of Things (IoT) and Cyber-Physical Systems (CPS) demand more intelligent and flexible agents that can dynamically update themselves without incurring downtime. Researchers have spent tremendous efforts to enable dynamic updating for programs developed in mainstream languages such as C and Java. One challenge in this appealing technique is that the correctness of dynamic updating is difficult to guarantee, which consequently limits its application in practice. In this paper, we propose a unified operational semantics-based approach to formalize and verify dynamic software updating. In the approach, dynamic updating strategies are formalized as a set of executable rewrite rules, seamlessly with the definition of the operational semantics of the target language. From the formalization several formal tools are automatically yielded, with which we can verify the properties of dynamic updating. We demonstrate the feasibility of the approach by formalizing a typical DSU tool Ginseng using a formal semantic framework--K.