1 Introduction

Software systems require frequent updating to fixate defects, improve performance, and add new features. For those systems providing \(24\times 7\) service commitment, Dynamic Software Updating (DSU) is a useful technique as it does not incur system downtime while updating [5]. Such systems are becoming prevalent with the diffusion of Internet of Things (IoT) and Cyber-Physical Systems (CPS), where additions, modifications, and removal of behaviors could be done in a quick and localized fashion. There is a comprehensive survey on DSU [10].

The difficulty of guaranteeing the correctness of dynamic updating is a fundamental barrier when we adopt this technique widely as expected. Correctness is crucial to those systems that need dynamic updating because they are usually safety-critical and highly-dependable. Meanwhile, dynamically updating a running software system is a complicated process, and it is difficult to predict all possible updating results. In order to update a program successfully while it is running in practice one has to know everything about that program [6]. However, it still lacks effective methodologies and tools to help understand all possible behaviors of running programs caused by updating.

Formal methods are rigorous approaches to program verification. Some attempts have been made on applying formal methods to DSU [3, 4]. The existing approaches suffer one or more difficulties as follows. In some approaches formalizing a dynamic update may require abstraction of target programs. Such abstraction is usually done manually. It requires both formal methods expertise and human intellection to interpret target programs. Some approaches [1, 11] lack tool support while developing such tools needs substantial efforts.

To mitigate the above difficulties, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs in this paper. KupC is built upon the formalization of a DSU tool called Ginseng [8] for C programs. We formalize the updating strategy of Ginseng atop the operational semantics of C in the formal semantic framework called \(\mathbb {K}\) [9]. From the formalization, \(\mathbb {K}\) automatically generates several tools that can be used for formal analysis of dynamic updating of C programs. According to our knowledge, KupC is the first tool for the code-level formal verification of dynamic software updating.

KupC has the following three features. (1) KupC is focused on the code-level verification of dynamic updating. It does not require any abstraction or transformation of target C programs that are subject to dynamic updating. (2) The verification functionalities of KupC are automatically generated from the formalization of dynamic updating mechanisms. No extra effort is needed on the implementation. (3) The formalization is built upon the operational semantics of the C language. One can easily develop similar tools for the formal analysis of dynamic updating of other languages such as Java and Python, whose operational semantics have already been formally defined in \(\mathbb {K}\).

2 KupC Design

Patch-based DSU. Many DSU tools achieve dynamic updating by injecting patches into running programs [10]. A patch contains all updating contents, e.g., new functions and data. Figure 1 (left) is an overview of the patch-based updating process. An old-version program is first made updatable by attaching additional version information, wrapping user-defined types, and inserting possible updating points. They are achieved by the two operations called Dependants Updating and Restriction Generating. Next, a patch file p1.c is generated and complied by comparing the differences between old and new programs. After an update request is invoked, a DSU tool checks whether it is safe to inject the compiled patch whenever the running program reaches a pre-specified updating point. Safety means that the behavior of the updated program is consistent with the expectation. It is guaranteed by the adopted updating policies in DSU tools. If it is safe, the patch is injected and the running program state is transformed into the new version by a transformation function that is predefined in the patch. The patched program continues to execute from the new state. If updating at this point is not safe, the program continues to execute the old version.

It is worth mentioning that the entire updating process is atomically performed, that is, the execution keeps being suspended until the completion of the updating. Updating in an atomic manner is the most consistent approach that simplifies the updating process and reduces unexpected errors.

The \(\mathbb {K}\) Framework. \(\mathbb {K}\) [9] is a state-of-art semantic framework for programming languages. Many mainstream languages such as C and Java have been completely defined in \(\mathbb {K}\). One only needs to focus on the formalization of an updating mechanism using the pre-defined operational semantics of the targeted language. After formalizing the updating mechanism, \(\mathbb {K}\) automatically generates several analysis tools such as program interpreter, state space explorer, and model checker.

Fig. 1.
figure 1

Patch-based dynamic updating and its formalization using \(\mathbb {K}\)

Full size image

Formalization of dynamic updating strategy in \(\mathbb {K}\). The basic idea of formalizing a dynamic updating mechanism using \(\mathbb {K}\) is to formalize the functionalities of the mechanism on the basis of the operational semantics of the target programming language that the mechanism supports. The right part of Fig. 1 shows the formalization of the patch-based dynamic updating mechanism, consisting of the formalization of the five functionalities, respectively.

The functionalities of an updating mechanism are formalized by a set of rewrite rules. For instance, below is a rewrite rule that formalizes the function of checking the safety of updating a set of functions at an updating point Loc.

figure a

In the rule, a pair of brackets is a labeled cell, representing a piece of program execution information. \(\frac{F}{\cdot }\) means F is deleted from the set if the conduction that follows the keyword when is true. The condition says that either F is updatable (represented by \(F\not \in Re\)) or it is un-updatable at the point \( Loc \) but its types T and \(T'\) (before and after updating, respectively) are the same. Here, Re is the set of un-updatable contents at Loc. If the second argument of \( TypeSafety \) becomes an empty set, it means all the functions in the set are safe to update.

We totally defined 371 rewrite rules to formalize the updating mechanism of Ginseng. We tested the correctness of the rules using the example dynamic updating programs provided in Ginseng. These rules are seamlessly compiled by \(\mathbb {K}\) together with the rules defined for the operational semantics of C [2]. The compilation yields the formal tool KupC which supports formal analysis of dynamic updating of C programs in various ways such as simulation, state exploration, and LTL model checking.

3 KupC Usage

KupC is equipped with an interpreter to execute updatable C programs, a state space explorer to search for all possible updating results, and an LTL model checker to verify temporal properties of dynamic updating. We demonstrate the usage of KupC using a dynamic updating to a GPS application. The tool, examples and a demo video are available https://github.com/dexter-qjq/KupC.

The program in Fig. 2 (left) is the old version of a GPS system. It calculates the shortest path. In the new version in Fig. 2 (right), the new program not only shows the shortest path, but also finds the most economic path. Three update points are inserted in function Query from Line 24 to Line 30.

Fig. 2.
figure 2

The snippets of old-version and new-version programs of a GPS application

Full size image
Fig. 3.
figure 3

The shortest path before and after updating (Color figure online)

Full size image

Simulating a dynamic updating scenario. Given an original C program annotated with update points, KupC can compile it with a patch file and generate binary code that is executable on \(\mathbb {K}\). During execution, updating is applied once reaching a safe updating point. It simulates the behavior of a dynamic updating to a program that is running on a real-world operating system.

Figure 3 shows the results of the simulation. Figures 3(a) and (b) show the original graph and the updated graph, respectively. When the update takes place at point1, the output of first call is the red path in Fig. 3(a). While the second call produces two paths as shown in Fig. 3(b). The red one is the shortest path and the green one is the most economic path.

Fig. 4.
figure 4

All possible updating results searched by the state space explorer of KupC

Full size image

Exploring all dynamic updating results. In addition to simulating one possible updating scenario, KupC can search for all possible updating results by exploring each possible updating point using the state space explorer.

We compile and execute the program map with the option UPSEARCH=1 to invoke the state exploration function. Figure 4 shows all five different updating results. The outputs are divided into two parts by semicolon, representing the results of the two function calls of Query, respectively. Case 1 and Case 2 show the results when updating occurs at point1. Case 3 and Case 4 are for point3. Case 4 shows the result when updating is not performed.

While the dynamic updating occurs during the first call of the function Query at point3 in Case 3, the output of the first call is not affected by updating. The reason is that the updated content will not take effect until the next access after updating. Therefore, the outputs in Case 4 are exactly the same as the ones in Case 5. Updating at point2 violates the safety policies. Therefore, there is no case corresponding to point2. All the updating results searched are valid.

Model checking temporal properties. Dynamic updating is a temporal behavior in that the properties before and after updating may be different. Such differences can be formalized as temporal properties. Another attractive function of KupC is to verify these temporal properties using LTL model checking.

As an example, we verify whether or not updating in the GPS example can be finally deployed. First, we introduce an atomic proposition called , which is false before updating and becomes true after the program is updated. Given the command , KupC returns true, indicating that updating can be eventually performed.

Another property of interest is that the shortest path must become 7 after the system is updated. It can be defined as an LTL formula , where variable x stores the value of the shortest path. Given the command , KupC returns true, indicating that updating result is correct as expected.

4 Concluding Remarks and Ongoing Work

We have presented the design and implementation of an operational semantics-based verification tool called KupC for dynamic software updating. Three case studies showed the effectiveness of KupC for the formal analysis of the dynamic software updating of C programs by simulation, state exploration, and LTL model checking. Semantics-based formalization is promising in providing effective and practical solutions for guaranteeing the correctness of dynamic software updating. For instance, Lounas et al. achieved formal verification of dynamic updating of Java programs based on Java’s semantics [7]. Compared with their approach, our approach is more general and extendable as \(\mathbb {K}\) provides an elegant semantic framework for the definition of programming languages and an easy-to-use automated verification tool generation service.

KupC is at a good position for practical code-level verification of DSU. It is directly applicable to the code and shows the feasibility of formalizing a dynamic updating mechanism on the basis of the operational semantics of target programming languages. To verify the dynamic updating of more complex and practical programs, a complete semantics of C including those of standard libraries is needed. The efficiency of KupC also needs to examine although the efficiency of \(\mathbb {K}\) has been validated [9]. There is ongoing work on these directions.

KupC has some limitations because of theoretical and practical challenges in the formal verification of DSU. Theoretically, Gutpa et al. have shown the undecidability of the reachability of updating points [3]. Another issue is that there is no uniform definition of correctness of dynamic updating. The logical correctness of dynamic updating depends on target programs and its formalization relies on programmers’ interpretation. Although KupC does not require any abstraction of target programs, we suspect that certain abstraction is necessary for optimizing efficiency and scalability of the verification. For instance, a function that is not modified in a new version can be considered atomic for verification purpose. It is still an ongoing quest for an appropriate abstraction of target programs for the scalability while maintaining the validity of verification.