A Unified Operational Semantics-based Approach To Modeling And Verifying Dynamic Software Updating

Dynamic software updating(DSU)is an efficient way of software updating without incurring any downtime.Traditional software updating needs to shut down the software first,install the new version,and finally execute the new version program.Dynamic software updating refers to the upgrade of software in the process of software running.With the rapid development of information technology in society,various software systems play a very important role in all aspects of social life.Dynamic updating is particularly important for those software systems that require 24×7 uninterrupted services,such as cloud computing,network services and financial industry systems.Interrupting the execution of such programs can be costly.At the same time,with the development of Cyber-Physical Systems(CPS)and Internet of Thing(IoT),the demand for more flexible and intelligent software systems that can be dynamically updated is expanding.DSU has been intensively studied in the past decades.Researchers have proposed a number of approaches and built many kinds of prototypical tools to support dynamic updating.Programs written in many mainstream programming languages such as C or Java can be dynamically updated using specialized DSU tools.However,dynamic software updating has not been widely applied as expected,the most important reason is that it is difficult to ensure the correctness of the updating.While the correctness is crucial to dynamic updating because the typical systems that require this technique are usually safety-critical and highly-dependable.In this paper,we propose a unified operational semantics-based approach to modeling and verifying dynamic software updating at code level.We implement our approach using K–a rewrite-based executable semantic framework for programming language.In our approach,dynamic updating strategies are formalized as a set of executable rewriting rules,seamlessly with the definition of the operational semantics of the target programming language.Many programming languages are completely defined in K,such as C,Java and Python.It is convenient to formalize DSU mechanism based on the definitions of these operational semantics.The formalization automatically yields several verification tools by K,which can be used to formally analyze the correctness of dynamic updating such as an interpreter for running the updatable programs,a explorer for searching the state space and a LTL model checker for checking the required temporal properties.Finally,we apply our approach to develop a formal tool for verifying the dynamic updating for C,K??C,and demonstrate the feasibility of the tool by several examples.To our knowledge,K??C is the first formal tool for code-level verification of dynamic software updating.