Exact acceleration of complex real-time model checking based on overlapping cycle

Introduction

In real-time embedded systems, especially complex real-time control systems, discrete logic control and continuous time behavior depend on and influence each other. Take the Internet of things (IoT) gateway security system (Wang et al., 2018) as an example: its control center generally has many different control modes to deal with diverse security risks, such as tampering, intrusion, and identity forging. Important system parameters (e.g., sensor status, monitoring instructions, and terminal feedback information) change continuously over time. To meet specific time constraints or parameter values in the IoT gateway security system, the management mode must be adjusted over time. The change rules of important parameters also differ by mode, and the response time to various events should be modified accordingly. In this type of system (Lee et al., 2019), logic control describes the logical control transformation of the system through models with high abstraction levels, such as finite state machine and Petri net. Time behavior can be simulated by clock variables and clock zone transformation. Between the two layers, signals of the continuous layer and control modes of the discrete layer are correlated and transformed by certain interfaces and rules.

Typically, test and simulation technologies are the main means of guaranteeing software quality; however, they cover problems when using the operating system as the main measure, which cannot guarantee test completeness. These approaches are thus incapable of traversing all states in a real-time system, leading to covert problems in system operations (Wang, Pastore & Briand, 2019). In the field of security-related systems with zero tolerance for system error, using formal theory and technology for security authentication results in clear descriptions and avoids the complexity of safety verification. Formal description analysis and refinement have thus become a focus of recent research in related fields.

In real-time model checking, timed automata can model the temporal behavior of real-time systems (Pinisetty et al., 2017). Clocks describe the state transitions, and clock constraints serve as the theoretical basis for real-time system model checking (Han, Yang & Xing, 2015). This approach can easily realize automatic combination and transformation with other methods. The method is widely used in polling control systems, railway interlocking systems, and similar applications. Due to clock variables, control programs and external environments often use different time measures, which can cause the number of states to increase exponentially when a timed automaton is transformed into a zone automaton. The reachability analysis algorithm generates many state fragments (Iversen et al., 2000; Chen & Cui, 2016), resulting in a sharp increase in the state space and considerably prolonged detection time.

The acceleration technique is a reduction method used to solve the fragmentation problem following from time measurement differences. Dubout & Fleuret (2013) applied an acceleration technique to linear target detection and effectively improved the detection performance. Jeong et al. (2014) applied an implicit Markov model as an improved framework to accelerate the inference model. For distributed and parallel computing, a workstation and a multicore processor were used to accelerate state-space searching (Konur, Fisher & Schewe, 2013). Lin, Chen & Xu (2017) studied an acceleration model using a Bayesian classifier by analyzing the behavior of heterogeneous population trends; results indicated that acceleration in the reliability assessment improved the analytic accuracy. The model checking of linear temporal logic (LTL) model was studied by Barnat et al. (2010), which employed computed unified device architecture for acceleration. Two SAT problem solvers were used to validate online models and accelerate the processing of complex behaviors (Qanadilo, Samara & Zhao, 2013).

The reachability problem is the first to consider in timed automata, which determines whether a path exists from its initial state to a target state. This problem can be solved by computing the zones that apply the abstraction technique in practice. State-of-the-art abstraction methods (Behrmann et al., 2006; Herbreteau, Srivathsan & Walukiewicz, 2016) produce an approximation closer to the actual reachable clock valuation, which includes coarser abstractions. Exact acceleration is an excellent means of abstraction to reduce required storage space and can alleviate state-space explosion. For practical issues such as protocol validation (Zhang et al., 2013), IoT system modeling (Li et al., 2013), and smart contract security verification in blockchain (Cruz, Kaji & Yanai, 2018; Grishchenko, Maffei & Schneidewind, 2018), exact acceleration technology is an efficient way of minimizing required storage space and time.

When Iversen et al. (2000) used UPPAAL to verify the LEGO robotic system, a fragmentation problem was identified and briefly described, and some ideas for further research were suggested. An approximation technique was applied to a real-time system model for security and connectivity analysis, which avoided repetitive control (Möller, 2002). After that, a real-time property language L_∀S was proposed to check the rejection state of reachability and reduce safety and boundary liveness simultaneously (Aceto et al., 2003). The problems and methods in these publications have promoted the concept of exact acceleration and inspired further research. Related studies on exact acceleration in real-time model checking include Hendriks & Larsen (2002), Yin, Song & Zhuang (2010), Yin, Zhuang & Wang (2011), Gou et al. (2014), Boudjadar et al. (2016), and Chadli et al. (2018). In the following four examples, the window of the acceleratable cycle is [a, b].

• Hendriks & Larsen (2002) introduced a method of syntax adjustment to a subset of timed automata by adding an appended cycle whose length was $⌈a∕\left(b-a\right)⌉$ times longer than that of the acceleratable cycle. This method accelerates forward symbolic reachability analysis, which solves the fragmentation problem and optimizes the verification of the LEGO robotic system.

• Yin, Song & Zhuang (2010) proposed a method to identify the acceleratable cycle in timed automata by introducing topological sorting for a large state space of a timed automaton; by simplifying the scale of timed automata, the method operated efficiently.

• An exact acceleration method based on a parking cycle was proposed (Yin, Zhuang & Wang, 2011), in which the entry boundary condition was determined by the size of the acceleratable cycle’s window (the condition is $z\ge a\times \frac{a}{b-a}+n_0$); the automaton model improved the speed of exact acceleration and reduced the cost.

• By analyzing the main parameters of the acceleration process, Gou et al. (2014) proposed a method for determining whether exact acceleration was required. This approach can be used to avoid adding an appended cycle to reduce verification speed when the number of fragments is small, or fragments do not satisfy certain conditions.

• Boudjadar et al. (2016) proposed a development method to improve the utilization rate of resources by using model-checking technology. In the design and development stage, exact acceleration technology was used to greatly improve the capability of symbolic model checking in a processing scheduling system. For the scheduling problem of network physical systems, Chadli et al. (2018) modeled advanced specifications and validation frameworks with the help of exact acceleration technology, automatically transforming high-level specifications into formal models. The above two research works mainly applied exact acceleration to model a system resource scheduling problem but did not improve the original exact acceleration theory.

When modeling a complex real-time system (Wang et al., 2019), multiple acceleratable cycles may overlap at the same location. If the appended cycle method is used for exact acceleration, then the added locations multiply as the number of acceleratable cycles increases, resulting in insufficient memory for model checking. If the parking cycle method is used for exact acceleration, acceleratable-cycle stacking leads to non-uniformity in parking-cycle entry conditions; differences in the windows of multiple acceleratable cycles can increase time consumption drastically. In this paper, we propose an exact acceleration method for complex real-time model checking based on an overlapping cycle, which is an application scenario extension of parking-cycle technique. A single overlapping cycle is developed by comprehensively analyzing the accelerating effects of multiple acceleratable cycles and analyzing acceleration differences among these cycles. The overlapping cycle is simple to create and has a fixed length, eliminating the need to add multiple locations for complex real-time models. The overlapping cycle adds much less state space than appended cycles or parking cycles in model checking, substantially reducing the acceleration cost. The proposed method can be effectively applied to modeling and verification of complex real-time systems such as the IoT gateway security system. It can also alleviate additional consumption of time and space caused by state-space explosion while maintaining the original nature of the system.

The remainder of this paper is organized as follows. The section ‘Preliminaries’ briefly introduces timed automata, forward symbolic reachability analysis, and the theory of exact acceleration. The exact acceleration method for complex real-time models based on an overlapping cycle is proposed in ‘Exact Acceleration of Complex Real-time System Model Based on Overlapping Cycle’, which outlines the method of creating a single, fixed-length overlapping cycle. A timed automaton with an overlapping cycle is shown to accelerate the originally timed automaton with reachability. In ‘Experimental Results’, the acceleration effects of the appended cycle, parking cycle, and overlapping cycle with a complex real-time model example are compared using experiments. Finally, the ‘Conclusion’ provides a few ideas for future research.

Preliminaries

Timed automata

This part is based on work by Alur & Dill (1994). To illustrate the real-time clock of timed automata more clearly, we define a clock constraint set T(C) contain all clock constraints. We assume that the set of clock variables is C, and the definition of the set of clock constraints τ is as follows: ${\displaystyle \tau :=c\sim n|{\tau }_1\wedge {\tau }_2}$ where c ∈ C, n ∈ ℕ, and ∼ denotes one of the binary relationships $\left\{<,\le ,=,\ge ,>\right\}$. The clock constraint set T(C) is the set of all clock constraints τ.

A clock interpretation ν is a mapping from C to ${\mathbb{R}}^{+}\cup \left\{0\right\}$, where ℝ⁺ represents the set of positive real numbers. Note that ν assigns each clock variable in the set of clock variables C. For a set X⊆C, X: = 0 indicates that X assigns 0 to each c ∈ X (i.e., clock reset), whereas the clock variables in set C − X have no effects.

Definition 1 (Timed automaton). A timed automaton is defined as a six-tuple (C, L, L₀, A, I, E), where C is a set of clocks, L is a finite set of locations, L₀⊆L is the set of initial locations, A is a set of action events, I represents mapping that provides every location l ∈ L with some clock constraint in T(C), and E⊆L × A × T(C) × 2^C × L is a set of edges. An edge (l, a, τ, λ, l′) denotes a transition: when the clock constraint in location l satisfies τ, the system can complete action event a, move from location l to location l′, and allow clocks in λ to be reset.

Figure 1 shows an example of a timed automaton. The timed automaton M represents a plain and abstract model of the control program and the external environment in a real-time system. If the control program sends instructions to the control center in an IoT security system, the environment will be decided by sensors and actuators. The cycle of locations L1, L2, and L3 model the control program labeled the control cycle, consisting of three atomic instructions, whose clock is x. The external environment is modeled by clock y, which is checked each time in L2. The clock y also called global clock. The size of the threshold constant LARGE determines how slow the environment is relative to the control program. If y ≥ LARGE, the control cycle may be exited.

The semantics of a timed automaton M is defined by a transition system S(M) with Alur & Dill (1994). A state of S(M) is a pair $\left(l,\nu \right)$, where l is a location of M and ν indicates a clock interpretation for C such that ν satisfies I(l). Regarding this transition system, the traces of a timed automaton have been defined by Hendriks & Larsen (2002).

Exact acceleration

Hendriks & Larsen (2002) proposed the concept of exact acceleration, based on which, we provide basic definitions for our study. The acceleratable cycle is a key concept in exact acceleration. An acceleratable cycle can use only one clock in clock constraints (including invariants, guards, and resets).

Definition 2 (Acceleratable cycle). Let M = (C, L, l₀, A, I, E) be a timed automaton, E_c = (e₀, …, e_n−1) ∈ Eⁿ, and x ∈ C. An acceleratable cycle is defined as a two-tuple (E_c, x) when the following conditions are satisfied:

• E_c is a cycle;

• for all locations in E_c, I(l) is either empty or in the form of {x ≤ c};

• if (l, a, τ, λ, l′) ∈ E_c, then τ is empty or in the form of {x ≥ c}, and λ is empty or only contains x; and

• x must be reset on all in-going edges to src(e₀).

Clock x is the clock of the cycle, $I\left(l\right)$ is the location invariant, and τ is the edge guard. The location src(e₀) is the reset location whose out-going edge is e₀, which indicates the external clock’s checking position in the acceleratable cycle. If a specific location’s in-going edge is e_i in the cycle, then the out-going edge of this position is e_i+1, where i ∈ [0, n − 2].

The cycle in automaton M (Fig. 1), composed of locations L1, L2, and L3, is an acceleratable cycle. The clock of the cycle is x, and the reset location is L2. The invariants and guards are in accordance with the defined form of clock x, and the clock resets to zero at the only in-going edge of L2.

Definition 3 (Window of acceleratable cycle). Let an acceleratable cycle in the timed automaton M be (E_c, x). The compression sequence of all traces is expressed as $T_r\left(E_c\right)=\left(\left(l_0,{\nu }_0\right),\left(l_0,{\nu }_0^{{}^{\prime }}\right),\left(l_1,{\nu }_1\right),\dots ,\left(l_{n-1},{\nu }_{n-1}\right),\left(l_{n-1},{\nu }_{n-1}^{{}^{\prime }}\right),\left(l_n,{\nu }_n\right)\right)$, where ν_i and ${\nu }_i^{{}^{\prime }}$ indicate different clock interpretations, i ∈ [0, n], and l₀= l_n= $src\left(e_0\right).\left(\left(l_j,{\nu }_j^{{}^{\prime }}\right),\left(l_{j+1},{\nu }_{j+1}\right)\right)$ depends on the edge e_j and can be understood as an action event of e_j, j ∈ [0, n − 1]. The window of the acceleratable cycle (E_c, x) is defined as the interval [a, b], a, b ∈ ℕ when the following conditions are satisfied:

• the total delay of T_r(E_c) is an element of [a, b]; and

• for any real number d ∈ [a, b], we adjust the delays under legal clock constraints in T_r(E_c) to ensure the total delay is d.

The meaning of the total delay in this definition is an increase in the clock of the cycle, which can be simply defined as the increment of the external clock when the acceleratable cycle returns to the reset location once from the initial location. The window is the minimal and maximal time it may take to pass through a cycle. According to this definition, the window of the acceleratable cycle shown in Fig. 1 can be calculated as [3, 7].

Definition 4 (Accelerated automaton based on appended cycle). Let $M=\left(C,L,l_0,A,I,E\right)$ be a timed automaton, and let Cycle = (E_c, x) be an acceleratable cycle of M, where L= $\left\{l_0,l_1,\dots ,l_m\right\}$, E_c = $\left(e_0,e_1,\dots ,e_{n-1}\right)$, e_i= (l_i, a_i, τ_i, λ_i, l_i+1). Acceleration of M based on the appended cycle is a new automaton Acc_a(M, Cycle) defined as (C, L′, l₀, A, I′, E′), where

• $L\prime =L\cup \left\{l_1^{\prime },l_2^{\prime },\dots ,l_{n-1}^{\prime }\right\}\cup \left\{l_0^{\prime }\right\}\cup \left\{l_1^{″},l_2^{″},\dots ,l_{n-1}^{″}\right\}$

• $I^{\prime }\left(l_i\right)=I\left(l_i\right)$, 0 ≤ i ≤ m

• $I^{\prime }\left(l_i^{\prime }\right)=I\left(l_i\right)$, 1 ≤ i ≤ n − 1

• $I^{\prime }\left(l_0^{\prime }\right)=\varnothing$

• $I^{\prime }\left(l_i^{″}\right)=I\left(l_i\right)$, 1 ≤ i ≤ n − 1

• $E^{\prime }=E\cup \left\{\left(l_0,a_0,{\tau }_0,{\lambda }_0,l_1^{\prime }\right),\left(l_{n-1}^{\prime },a_{n-1},{\tau }_{n-1},{\lambda }_{n-1},l_0^{\prime }\right)\right\}$ $\cup \left\{\left(l_0^{\prime },a_0,{\tau }_0,{\lambda }_0,l_1″\right),\left(l_{n-1}″,a_{n-1},{\tau }_{n-1},{\lambda }_{n-1},l_0\right)\right\}$ $\cup \left\{\left(l_i^{\prime },a_i,{\tau }_i,{\lambda }_i,l_{i+1}^{\prime }\right),\left(l_i″,a_i,{\tau }_i,{\lambda }_i,l_{i+1}″\right)|1\le i\le n-1\right\}$

• in particular, $E^{\prime }=E\cup \left\{\left(l_0,a_0,{\tau }_0,{\lambda }_0,l_0^{\prime }\right),\left(l_0^{\prime },a_0,{\tau }_0,{\lambda }_0,l_0\right)\right\}$ when n = 1.

Theorem 1. Let M = (C, L, l₀, A, I, E) be a timed automaton, and let Cycle = (E_c, x) be an acceleratable cycle of M with a window [a, b]. If φ is the reachability property of M, then ${\displaystyle 3a\le 2b\Rightarrow \left(M\models \phi \iff Ac{c}_a\left(M,Cycle\right)\models \phi \right).}$

Theorem 1 has been proved in Hendriks & Larsen (2002). In Definition 4, the appended cycle is obtained by expanding the acceleratable cycle twice. If the timed automaton M is added to the appended cycle by expanding the acceleratable cycle i times, then the precondition in Theorem 1 can be generalized to (i + 1)a ≤ ib.

Definition 5 (Accelerated automaton based on parking cycle). Let $M=\left(C,L,l_0,A,I,E\right)$ be a timed automaton, and let Cycle = (E_c, x) be an acceleratable cycle of M with a window of $\left[a,b\right]$, where L= $\left\{l_0,l_1,\dots ,l_m\right\}$, E_c= (e₀, e₁, …, e_n−1), e_i = (l_i, a_i, τ_i, λ_i, l_i+1). The global clock is y, and the maximum value of y before entering the acceleratable cycle is n₀. The acceleration of M based on the parking cycle is a new automaton Acc_p(M, Cycle) defined as (C, L′, l₀, A, I′, E′), where

• $L^{\prime }=L\cup \left\{l_0^{\prime }\right\}$

• $I^{\prime }\left(l_i\right)=I\left(l_i\right)$, 0 ≤ i ≤ m

• $I^{\prime }\left(l_0^{\prime }\right)=\varnothing$

• $E^{\prime }=E\cup \left\{\left(l_0,a_0,\tau \prime ,\varnothing ,l_0^{\prime }\right),\left(l_0^{\prime },a_{n-1},\varnothing ,{\lambda }_{n-1},l_0\right)\right\}$, τ′ is $y\ge a\times ⌈\frac{a}{b-a}⌉+n_0$.

Definition 5 has been given in Yin, Zhuang & Wang (2011). The accelerated automaton Acc_a(M, Cycle) equals the timed automaton M with an appended cycle composed of locations $l_0,l_1^{{}^{\prime }},l_2^{{}^{\prime }},\dots ,l_{n-1}^{{}^{\prime }},l_0^{{}^{\prime }},l_1^{{}^{\prime \prime }},l_2^{{}^{\prime \prime }},\dots ,l_{n-1}^{{}^{\prime \prime }}$. Accelerated automaton Acc_p(M, Cycle) equals the timed automaton M with a parking cycle whose edge guard y controls the acceleration timing. Only when the acceleratable cycle has been executed at least $⌈a∕\left(b-a\right)⌉$ times is the automaton permitted to enter the parking cycle. Figures 2 and 3 display the acceleration of M (Fig. 1) based on the appended cycle and parking cycle, respectively. They are labeled the accelerated automata M_a and M_p. Because the window of the acceleratable cycle is [3, 7], the edge guard of the parking cycle is y ≥ 3 in M_p.

Theorem 2. Let M = (C, L, l₀, A, I, E) be a timed automaton, and let Cycle = (E_c, x) be an acceleratable cycle of M with a window of [a, b]. If φ is a reachability property of M, then ${\displaystyle a<b\Rightarrow \left(M\models \phi \iff Ac{c}_p\left(M,Cycle\right)\models \phi \right).}$

Yin, Zhuang & Wang (2011) gives this theorem form forward symbolic reachability analysis, and this is the previous achievement of our working group. We will give its another proof in the view of zone later.

Exact Acceleration of Complex Real-time System Model Based on Overlapping Cycle

The appended cycle and parking cycle technologies in exact acceleration apply to a real-time system model with a single acceleratable cycle. For a complex real-time system model (as shown in Fig. 4), using these two technologies for exact acceleration requires additional states and consumes a large amount of time cost, which influences the acceleration effect.

Figure 4 presents an example of the IoT gateway security system (in Wang et al., 2018). The timed automaton M′ models a wireless sensor network including a reactive program and external environment. The run-time behavior control several sensors, which can be transformed into clock constrains in UPPAAL. Every location in the cycle represents a sensor model in the IoT system. The cycle’s clock is x, and clock y controls the execution time. The larger the constant LARGE is, the more slowly the timed automaton M′ runs. Using the algorithm described by Yin, Song & Zhuang (2010) to identify the acceleratable cycle in M′, we obtain four acceleratable cycles whose reset locations are all L1 and share the clock of cycle x. For this complex real-time model, we propose a method based on the overlapping cycle for exact acceleration.

Theorem 3. Let M = (C, L, l₀, A, I, E) be a timed automaton, and let Cycle = (E_c, x) be an acceleratable cycle of M with a window of [a, b]. If a < b, there is a positive integer n in the forward symbolic reachability analysis, which leads the reset location to obtain a continuous clock zone after executing the Cycle n times.

Proof. According to the forward symbolic reachability analysis, the problem of fragments in the acceleratable cycle will inevitably lead to the overlap of clock zones, that is, the appearance of continuous clock zone. If a < b, according to the definitions about exact acceleration, the continuous clock zone will be got after several executions of the acceleratable cycle, and the point of the proof is to determine the number of executions.

So, without loss of generality, we might assume that the execution number is a positive integer n. Let n be the rounds of Cycle execution, and let the interval [c, d] be the clock zone at the reset location before execution of the Cycle. At the reset location, the clock zone is continuous from the (n + 1)th time onward; therefore, the clock zones obtained in the (n + 1)th time and the nth time have an intersection that is ${\displaystyle \left(n+1\right)a+c\le nb+d\Rightarrow n\ge \left(a+c-d\right)∕\left(b-a\right).}$

Because b > a, d ≥ c, there must be an integer n ≥ a∕(b − a). So, the number of executions should be at least $⌈a∕\left(b-a\right)⌉$. When the Cycle is executed $⌈a∕\left(b-a\right)⌉$ (that is n) times, the reset location obtains a continuous clock zone, thereby completing the proof.

Corollary 1. If the timed automaton M has an acceleratable cycle with a window of [a, b], a < b, then the reset location will obtain a continuous clock zone after executing the Cycle at least a∕(b − a) times during forward symbolic reachability analysis.

Proof. According to Theorem 3, we easily know the reset location obtains a continuous clock zone when the Cycle is executed n times. For the integer n, we can calculate that n ≥ a∕(b − a). The proof is completed.

Corollary 2. Let the global clock be y, and let the maximum value of y before entering the acceleratable cycle be n₀. If the timed automaton M has an acceleratable cycle with a window of [a, b], a < b, then the reset location will obtain a continuous clock zone when the following condition is satisfied during forward symbolic reachability analysis: ${\displaystyle y-n_0\ge a\times a∕\left(b-a\right).}$

Proof. According to Corollary 1, the reset location will obtain a continuous clock zone after executing the acceleratable cycle at least a∕(b − a) times. Because the window of the acceleratable cycle is [a, b], the increment of y by executing the acceleratable cycle a∕(b − a) times is denoted as Δy ∈ [a × a∕(b − a), b × a∕(b − a)], where Δy = y − n₀. Therefore, when y − n₀ ≥ a × a∕(b − a), the reset location will obtain a continuous clock zone. The proof is completed.

Corollary 3. Let the global clock be y, and let the maximum value of y before entering the acceleratable cycle be n₀. If the timed automaton M has an acceleratable cycle with a window of [a, b], a < b, then every location in the acceleratable cycle will obtain a continuous clock zone when y − n₀ ≥ a × a∕(b − a).

Proof. Because clock y is not the cycle clock, any invariant or guard in the acceleratable cycle will not contain clock y according to Definition 2. Based on the theory of timed automata, clock y exhibits monotonous growth when the acceleratable cycle is executed. Thus, when y − n₀ ≥ a × a∕(b − a), per Corollary 2, the reset location begins to obtain a continuous clock zone, indicating that every location in the acceleratable cycle is reachable. At this point, a constant clock zone will also be received by any location in the acceleratable cycle, and the proof is completed.

Next, we will give the new proof of Theorem 2.

Proof. Sufficient Condition. The known condition is a < b. Because Acc_p(M,Cycle) is obtained by adding a parking cycle to M, the timed automaton M can clearly reach any reachable state in original model. The accelerated automaton Acc_p(M,Cycle) can also reach states by executing the same time trace; that is, the state transition system S(M) associated with M is included in the state transition system S(Acc_p(M,Cycle)) associated with Acc_p(M,Cycle).

Necessary Condition. The known condition is a < b. Let the global clock be y. When y < a × a∕(b − a) + n₀, the accelerated automaton Acc_p(M,Cycle) does not execute the parking cycle, and reachable states in Acc_p(M,Cycle) are also reachable in the timed automaton M. When y ≥ a × a∕(b − a) + n₀ (according to Corollary 3), every location in the acceleratable cycle of M will obtain a continuous clock zone; that is, after y ≥ a × a∕(b − a) + n₀ at any time, M can reach any location in the acceleratable cycle and Acc_p(M,Cycle) executes the parking cycle, satisfies the edge guards, and returns to the reset location of any state, which guarantees that M is always reachable.

In summary, when a < b, the accelerated automaton Acc_p(M,Cycle) does not change the reachability property φ of the timed automaton M, and the proof is completed.

According to our theorems and corollaries, we can prove that the exact acceleration method based on the parking cycle is more concise and effective than that based on the appended cycle. On one hand, there is no location invariant in the parking cycle to ensure the clock can stay in this location for acceleration; on the other hand, the parking cycle contains an edge guard to ensure that any location of the acceleratable cycle obtains a continuous clock zone, which provides reachability. In this way, the parking cycle accelerates the search for the symbolic state by controlling acceleration timing and ensures reachability of the timed automaton to realize exact acceleration. The exact acceleration method for the complex real-time model based on an overlapping cycle is an improved method based on the parking cycle. It attempts to extend the application field of exact acceleration technology to complex real-time model checking to improve efficiency and alleviate state explosion.

Theorem 4. Let M = (C, L, l₀, A, I, E) be a timed automaton with several acceleratable cycles. Let Cycle_i= (E_ci, x) be the ith acceleratable cycle of M with a window of [a_i, b_i], where i is a non-zero natural number. All acceleratable cycles affect the cycle of clock x, and their reset locations are uniform in l_reset ∈ L. There is a single acceleratable cycle whose effect is the most effective in obtaining a continuous clock zone than multiple acceleratable cycles.

Proof. Let $n_j=⌈\frac{a_j}{b_j-a_j}⌉\times a_j$, $n_k=⌈\frac{a_k}{b_k-a_k}⌉\times a_k$, where 1 ≤ j, k ≤ i, and j, k are non-zero natural numbers. Then, n_j and n_k represent the edge guard of the jth and kth acceleratable cycle, respectively, when adding a parking cycle. If these two acceleratable cycles are executed simultaneously, the edge guard can be expressed as $n_{jk}=⌈\frac{a_j+a_k}{\left(b_j-a_j\right)+\left(b_k-a_k\right)}⌉\times \left(a_j+a_k\right)$. The window of the ith acceleratable cycle is [a_i, b_i] as a known condition, where 0 ≤ a_j ≤ b_j, 0 ≤ a_k ≤ b_k, and there is a_j + a_k ≥ a_j, a_k.

We make $\frac{a_j}{b_j-a_j}=\frac{U}{V}$, $\frac{a_k}{b_k-a_k}=\frac{X}{Y}$, such that $\frac{a_j+a_k}{\left(b_j-a_j\right)+\left(b_k-a_k\right)}=\frac{U+X}{V+Y}$. We assume that $\frac{U}{V}$ is smaller, then $\frac{X}{Y}=$ $\frac{U+\mu }{V}$, μ ∈ ℝ⁺. Therefore, there is $\frac{U+X}{V+Y}=\frac{U+U+\mu }{V+V}=\frac{U}{V}+\frac{\mu }{2V}>\frac{U}{V}$; that is, $⌈\frac{U+X}{V+Y}⌉\ge ⌈\frac{U}{V}⌉$ and $⌈\frac{U+X}{V+Y}⌉\ge min\left(⌈\frac{U}{V}⌉,⌈\frac{X}{Y}⌉\right)$. In the positive-number condition, a larger number multiplied by a larger number is either equal to or greater than a smaller number multiplied by a smaller number; therefore, ${\displaystyle ⌈\frac{U+X}{V+Y}⌉\times \left(a_j+a_k\right)\ge min\left(⌈\frac{U}{V}⌉\times a_j,⌈\frac{X}{Y}⌉\times a_k\right)}$ which is n_jk ≥ min(n_j, n_k).

According to Corollary 1, the reset location will obtain a continuous clock zone after executing the acceleratable cycle, which has a smaller value of $⌈\frac{a_i}{b_i-a_i}⌉\times a_i$, $⌈\frac{a_i}{b_i-a_i}⌉$ times during forward symbolic reachability analysis. This solution is faster than using two acceleratable cycles simultaneously to obtain a continuous clock zone, and it is better than using the larger one.

By extension, when comparing any two acceleratable cycles, a shorter time cycle always obtains a continuous clock zone more quickly. When comparing all acceleratable cycles, we can achieve the most effective acceleratable cycle for exact acceleration. This result indicates that the acceleration effect of a single acceleratable cycle is more effective than that of multiple acceleratable cycles, thereby completing the proof.

Corollary 4. Let M = (C, L, l₀, A, I, E) be a timed automaton with several acceleratable cycles. Let Cycle_i= (E_ci, x) be the ith acceleratable cycle of M with a window of [a_i, b_i], where i is a non-zero natural number. All acceleratable cycles affect the cycle of clock x, and their reset locations are uniform in l_reset ∈ L. If a_i < b_i, then the acceleratable cycle with the $min\left(⌈\frac{a_i}{b_i-a_i}⌉\times a_i\right)$ has the best acceleration effect of obtaining a continuous clock zone in the shortest time.

Proof. According to Theorem 4, comparing any two acceleratable cycles, a cycle with smaller value of $\left(⌈\frac{a_i}{b_i-a_i}⌉\times a_i\right)$ always obtains a continuous clock zone more quickly. When comparing all acceleratable cycles, the cycle with the $min\left(⌈\frac{a_i}{b_i-a_i}⌉\times a_i\right)$ obviously has the most effective acceleration. The proof is completed.

Definition 6 (Accelerated automaton based on overlapping cycle). Let M = (C, L, l₀, A, I, E) be a timed automaton with k acceleratable cycles, where L = {l₀, l₁, …, l_m}.CYCLE = {Cycle₁, …, Cycle_k|k ∈ ℕ⁺} denotes the acceleratable cycle set. Let Cycle_i = (E_ci, x) be the ith acceleratable cycle with a window of [a_i, b_i], where 0 ≤ i ≤ k, E_c= (e₀, e₁, …, e_n−1), e_ji= (l_ji, a_ji, τ_ji, λ_ji, l_(j+1)i). All acceleratable cycles affect the cycle of clock x, and their reset locations are uniform in l_reset ∈ L. The global clock is y, and the maximum value of y before entering the acceleratable cycle is n₀. The acceleration of M based on the overlapping cycle is a new automaton Acc_o(M, CYCLE) defined as (C, L′, l₀, A, I′, E′), where

• $L^{\prime }=L\cup \left\{l_{reset}^{\prime }\right\}$

• $I^{\prime }\left(l_h\right)=I\left(l_h\right)$, 0 ≤ h ≤ m

• $I^{\prime }\left(l_{reset}^{\prime }\right)=\varnothing$

• $E^{\prime }=E\cup \left\{\left(l_{reset},\varnothing ,{\tau }^{\prime },\varnothing ,l_{reset}^{\prime }\right),\left(l_{reset}^{\prime },\varnothing ,\varnothing ,{\lambda }^{\prime },l_{reset}\right)\right\}$, τ′ is $y\ge min\left(⌈\frac{a_i}{b_i-a_i}⌉\times a_i\right)+n_0$ and λ′ only contains x.

The accelerated automaton Acc_o(M, CYCLE) equals the timed automaton M with the addition of an overlapping cycle at only one reset location, which solves the problem where an exact acceleration cannot be used directly for complex real-time model checking. The overlapping cycle only needs to analyze all windows of every acceleratable cycle in CYCLE for the calculation. We can also avoid using an appended cycle or parking cycle for each acceleratable cycle, greatly reducing the additive symbolic state. Figure 5 depicts the acceleration of M′ (Fig. 4) based on an overlapping cycle, named accelerated automaton $M_o^{{}^{\prime }}$. Because the timed automaton M′ contains four acceleratable cycles, we analyze them separately, discard the deadlocked cycle, and only retain three executable cycles. The deadlocked cycle consists with location l₁, l₂, l₃, l₄, l₅, l₆, l₇, l₈, l₉, l₁₀, l₁₄, l₁₃, l₁ in sequence. For further analysis, the windows of acceleratable cycles are calculated as [7, 18], [6, 16], and [13, 24]. By taking the minimum value of $⌈\frac{a_i}{b_i-a_i}⌉\times a_i$, we can obtain the overlapping cycle’s entry condition, which is y ≥ 6.

Theorem 5. Let M = (C, L, l₀, A, I, E) be a timed automaton with several acceleratable cycles. Let Cycle_i = (E_ci, x) be the ith acceleratable cycle of M with a window of [a_i, b_i], where i is a non-zero natural number. If x is reset on edge e₀, then the subsequent states of src(e₀) reachable by multiple acceleratable cycles in M, are reachable by exactly one execution of the overlapping cycle in Acc_o(M, CYCLE).

Proof. For a certain acceleratable cycle, its window is set as $\left[a^{\prime },b^{\prime }\right]$. According to Theorem 1, when 3a′ ≤ 2b′, the appended cycle does not change the subsequent reachability of the reset location src(e₀) in M. According to Theorem 2, when a′ ≤ b′, the parking cycle does not change the subsequent reachability of the reset location src(e₀) in M. In the case of multiple acceleratable cycles superimposing on the same location in a complex real-time system, the subsequent reachability of the reset location src(e₀) in M can be guaranteed to remain unchanged if any part of the acceleratable cycle is processed with exact acceleration.

According to Theorem 4, the accelerable cycle is more effective for obtaining a continuous clock zone at reset location src(e₀) than multiple acceleratable cycles. In particular, according to Corollary 4, if a_i < b_i, then the exact acceleration based on overlapping cycle can obtain the continuous clock zone in the shortest time. The proof is completed.

This theorem ensures the effectiveness of acceleration. For a single acceleratable cycle, if all states are reachable by more than one execution of the acceleratable cycle, then exactly only one execution of the acceleratable cycle of the appended cycle or parking cycle can guarantee reachability of all states in the accelerative automaton. The complex real-time model checking differs from the exact acceleration of a single acceleratable cycle. In depth-first forward symbolic reachability analysis, it is necessary to verify whether subsequent states are reachable in priority while ignoring the breadth-first search within cycles.

In our case study of an IoT gateway security system (Wang et al., 2018), the control center must complete a security process and distribute it to each sensor node. Once a self-organizing sensor network completes the process, it can respond to the command of the control center in a timely manner. The control center can perform subsequent operations after receiving feedback regardless of whether other sensor nodes can complete the process. Hence, the security system must ensure its subsequent reachability regardless of who completes the process. This approach accelerates the search of subsequent states, thus avoiding time and space consumption caused by superposition of acceleratable cycles.

Experimental Results

To verify the validity of the exact acceleration method based on an overlapping cycle for complex real-time model checking, we collected runtime data, including memory consumption and verification time, from the timed automaton M′. We also gathered runtime data from the accelerated automata $M_a^{{}^{\prime }}$, $M_p^{{}^{\prime }}$, and $M_o^{{}^{\prime }}$, which use the appended cycle, parking cycle, and overlapping cycle, respectively. We employed the model-checking tool UPPAAL with a depth-first search order to verify whether location L15 was reachable, which can give the time and memory consumption in verification automatically. Experimental results are displayed in Table 2.

Results show that the time consumption of M′ increased with exponential growth of LARGE at a rate of nearly ten times without using exact acceleration. The memory consumption of M′ increased slightly because no additional locations were added. The accelerated automaton $M_a^{{}^{\prime }}$ used an appended cycle, which reduced the time consumption, reflecting the advantages of exact acceleration. However, due to a large number of additional locations, the memory consumption of $M_a^{{}^{\prime }}$ increased dramatically. The accelerated automaton $M_p^{{}^{\prime }}$ used a parking cycle to reduce the time consumption further compared to $M_a^{{}^{\prime }}$. The fixed length of the parking cycle reduced the number of additional locations compared to the appended cycle; accordingly, the memory consumption was much lower for $M_p^{{}^{\prime }}$ than for $M_a^{{}^{\prime }}$ but slightly higher than for M′. The accelerated automaton $M_o^{{}^{\prime }}$ that used the proposed overlapping cycle exhibited minimal time consumption and only required the addition of a single, fixed-length location for the complex real-time model. The memory consumption of $M_o^{{}^{\prime }}$ was close to that of M′, far less than that of $M_a^{{}^{\prime }}$, and slightly better than that of $M_p^{{}^{\prime }}$. We can explain the time and memory consumption of $M_o^{{}^{\prime }}$ by Theorem 5. The depth-first search order ensures that the overlapping cycle accelerates exploration before complete exploration of all accelerable cycles.

A less theoretical study case involves model verification of the IoT gateway security system (Wang et al., 2018). The exact acceleration method based on the overlapping cycle was successfully applied in this case, significantly improving verification efficiency. The technical framework of the IoT gateway security system is illustrated in Fig. 6.

An essential technology in the IoT gateway security system is the time-stamped advanced encryption standard algorithm. By introducing a timestamp into the key expansion phase, the round key can be dynamically updated with change over time to realize a cipher text change that ensures the security of confidential information. Due to the introduction of a timestamp, the system generates acceleratable cycles when modeled as timed automata. Multiple acceleratable cycles are overlaid on the same location in particular scenarios, which requires overlapping cycle technology for exact acceleration.

Our theory can be used to simulated the parallel execution of processes and idle cycles. However, the presence of urgent locations and synchronous channels may disturb exact acceleration. For example, if broadcast channel coordination occurs in an urgent location, the multi-party response of the broadcast should be completed before the next state location can be migrated. The execution time of the response process is not controlled by the cycle control program; thus, it is not appropriate to simply use exact acceleration technology for acceleration; the space–time loss of using acceleration technology should be compared to the broadcasting response. However, exact acceleration technology can often handle urgent locations and synchronous channels. The following case of an IoT gateway security system also involves these situations. As no extra time interference exists within the whole acceleration process, the exact acceleration technology can finally be successfully applied to system modeling and verification.

The accelerated automaton based on an overlapping cycle is an approximation that can be adapted to verify the accuracy of invariance and reachability properties. Consider the processes in Fig. 7; these processes model a top architecture and a middleware control program consisting of locations, edges, and channels.

The IoT gateway runs from the Start location, reads configuration information and performs gateway identity authentication. The underlying unified authentication service is invoked through channel StartAC for security authentication, and GatewayStatus is returned after authentication. If GatewayStatus =true, then the system enters the location EnterMiddle and transforms to the polling module of the middle layer through the StartMiddle channel. For the middle-layer polling module, polling begins through the StartMiddle channel, and the top-layer main module is returned by the FinishMiddle channel. Location CheckCategory controls whether polling logic ends up at a perception terminal or an execution terminal, which each have different processing methods. In the two polling processes, the underlying security service is invoked through the synchronization channel according to different requirements. The specific process can be interpreted by the meaning of state locations, synchronization channels, and variables as described by Wang et al. (2018). In particular, clock constraints are added during the stage of waiting for timing and the stage of keeping the equipment running. The top-layer main module model and middle-layer polling module model constitute the general framework of the IoT gateway security system. Security implementation depends on the underlying security service modules ultimately, hence it is necessary to improve model construction of the underlying security service modules. For complex system modeling with underlying services, we apply the exact acceleration method proposed in this paper, which can effectively improve the verification speed.

To demonstrate the effect of exact acceleration, we checked all security properties of the IoT gateway security system model in Fig. 7. Several examples are presented below.

(1) A[] not deadlock

Property 1 is used to check deadlock and ensure all state locations will be reachable.

(2) E<>Top.CheckGS

(3) E<>Top.EnterMiddle imply Middle.CheckCategory

Properties 2 and 3 are used to explore part of the state space. The truth of these two properties indicates that the implementation accelerated model is an exact acceleration with the overlapping cycle.

(4) A[] Top.Restart imply c<=300

(5) A[] Top.Record imply c<=600

(6) A[] Middle.RetrieveData imply Middle.y>=30

(7) A[] Middle.WaitDevice imply Middle.y<=5

Properties 4–7 are examined in terms of whether subsequent states of the reset location are reachable. Clock c is a global clock and clock y is used to model the duration of one process.

We measured time and memory consumption and explored states for these properties. The IoT gateway security system was modeled as a timed automaton M_IoT, and the acceleration of M_IoT with overlapping cycles was modeled as an automaton M_IoTo. We used model checkers UPPAAL and KRONOS to verify security system properties automatically, such as confidentiality, availability, and authenticity in parallel processes. KRONOS is able to complete the statistics of the state scale traversed by the whole verification process. It makes up for the fact that UPPAAL can’t do this. Table 3 lists the experimental results.

On the premise of guaranteeing the security of IoT gateway system, a large number of underlying services and various applications can be embedded in the system framework. At this time, the security requirements of IoT gateway system are mainly for various new access services, and the framework security of the gateway itself can be maintained by its own mechanism. After access to a large number of services and applications, the original model will become complex, concurrent, real-time with large-scale. The verification of the system needs to be processed by the exact acceleration method based on overlapping cycle.

With the increase of the number of access services, the system model becomes more and more complex, and the scale of access number greatly affect the efficiency of model verification. Appended cycle and parking cycle methods are more suitable for single accelerating cycle scenarios. In this complex scenario, when the number of services reaches a certain level, the acceleration process may not be completed. According to the change of the number of access services, Table 4 gives the comparison of the acceleration effects of different exact acceleration methods (from the perspective of time).

The results show that for complex real-time systems, the acceleration efficiency of overlapping cycle is much higher than that of appended cycle and parking cycle, and the verification can still be completed when the state scale reaches 10⁷ with proposed method. So, the exact accelerating technology substantially reduced the time required for verification in complex real-time model checking. Overlapping cycle acceleration demonstrated the highest efficiency compared to the appended cycle and parking cycle. In the simple example of automaton M′ in Fig. 4, 55 additional locations were required when using the appended cycle, much higher than the number of locations in the original model. Although the appended cycle reduced verification time, it increased the difficulty of adding locations to the model in an early stage. When many acceleratable cycles were stacked in the same reset position, more than one location needed to be added to M′ when the parking cycle was used, although the length of the parking cycle was fixed. The parking cycle was neither simpler nor faster than the overlapping cycle, and its previous calculation was larger than that of the overlapping cycle.

With the exception of this IoT case, our approach can be applied to other scenarios, such as security validation of blockchain smart contracts. The complete code and UPPAAL model can be found at https://github.com/iegqwang/UPPAAL.

Conclusions

To solve the fragmentation problem for complex real-time model checking, we propose an exact acceleration method based on an overlapping cycle, which is an application scenario extension of parking-cycle technique, to accelerate forward symbolic reachability analysis. Compared with the appended cycle or parking cycle for exact acceleration, the proposed method can be applied to the model acceleration of large-scale complex real-time systems and only requires the addition of a single, fixed-length location to the system’s timed automaton model. The addition of an overlapping cycle introduces far fewer symbolic states than using either an appended cycle or parking cycle. Rather than relying on windows of acceleratable cycles, the proposed accelerated automaton model is more straightforward and reduces the space–time overhead of exact acceleration.

Two aspects warrant exploration in future research. First, we must continue to study the algorithm for the acceleratable cycle, try to simplify the original automaton model, guarantee its original property, and rapidly identify the deadlock. Second, we plan to develop a simple exact acceleration automatic checking platform that can consider other practical conditions such as action transitions, urgent locations, and synchronous channels to solve actual modeling problems more efficiently.

Supplemental Information