This paper presents a real-time property specific reduction approach for Time Petri Net (TPN). It divides TPN models into sub-nets of smaller size, and constructs an abstraction of reducible ones, which exhibits the same property specific behavior, but has less transitions and states. This directly reduces the amount of computation needed to generate the whole state space. This method adapts well to the verification of real-time properties in asynchronous systems. It should be possible to apply similar methods to other families of properties.
The key issue that prevents a wide application of model checking in the industry
is the scalability with respect to the size of the target system. A realistic
system usually has thousands and even millions of states and transitions. Although
a huge part of impossible firing sequences of transitions are eliminated during
the building of system’s behavior, the interleaving of all others is still a very
large number that will easily lead to combinatorial state space explosion.
Classic verification methodologies usually encounter scalability issues very quickly
along with the growth of system scale, because they follow an implicit purpose:
many different kind of properties will be assessed relying on the same state space
graph (reachability graph). Indeed, once the reachability graph has been
generated, it can be reused to verify different kinds of properties, just by revising
the assessed logic formulas. This consideration requires to build the reachability
graph preserving precise and sufficient information for the assessment of
properties. The existing state space reduction methods, partial order reduction [
This work proposes a real-time property specific state space reduction approach for Time Petri Net (TPN). It divides the TPN model into sub-nets of smaller size, and constructs an abstraction of reducible sub-nets, which exhibit the same property specific behavior, but has less transitions and states. The real-time property specific behavior (called real-time behavior for short in the following parts) of TPN sub-nets is an abstraction of the whole state-transition traces that only preserves real-time behaviors from the viewpoint of observations. This method adapts well to the verification of real-time properties in asynchronous systems. It could be possible to apply similar methods to other families of properties.
This paper is organized as follows: Section 2 presents some related works; Section 3 introduces real-time properties and Time Petri Net; Section 4 gives an overview of property specific reduction methods; Section 5 defines two realtime behavior regularities for this work; Section 6 details the proposed reduction method; Section 7 provides experimental results; Section 8 discusses the behavior coverage issue; Section 9 gives some concluding remarks. 2
Several existing works [
The idea of our approach is similar to the partial order reduction [
The partial order reduction is usually used in asynchronous concurrent systems, where most of the activities in different processes are performed independently, without a global synchronization. Its main idea is to construct a reduced state class graph by analyzing the dependencies between the transitions and exploiting the commutativity of concurrently executed transitions, which result in the same state when executed in different orders. A set of non-reducible transitions are preserved in the reduced state class graph. The reduced behavior is a subset of the behavior of the full state class graph. Compared to the partial order reduction, the proposed property specific reduction exploits the commutativity of TPN sub-nets, which result in the same property specific behavior.
The TINA toolset provides various state space abstractions for TPN when
generating state class graphs, following the techniques proposed in [
Time Petri Net
Time Petri nets [
Definition 1 (Time Petri Net). A Time Petri Net (TPN) T is a tuple hP, T, •(.), (.)•, M0, (↵, )i, where: – P = {p1, p2, ..., pm} is a finite set of places; – T = {t1, t2, ..., tn} is a finite set of transitions; – •(.) 2 (NP )T is the backward incidence mapping; – (.)• 2 (NP )T is the forward incidence mapping; – M0 2 NP is the initial marking; – ↵ 2 (Q 0)T and 2 (Q 0 [ 1 )T are respectively the earliest and latest firing time constraints for transitions.
Following the definition of enabledness in [
Time Petri Net is widely used to formally capture the temporal behavior of concurrent real-time systems due to its easy-to-understand graphical notation and the available analysis tools, such as TINA, INA, Roméo, etc. 3.2
Real-Time Property Verification The safety and reliability of real-time systems strongly depend on the satisfaction of its real-time requirements, in both qualitative and quantitative aspects.
Dwyer et al. initially proposed qualitative temporal property patterns for
finite-state verification in [
Let’s first see an example benefiting from property specific reduction method. Example 1 (Example of Property Specific Reduction). When generating the reachability graph preserving markings for the TPN model in Fig. 1 by TINA, it contains 177 states and 365 transitions. This system is identified as two sub-nets A and B : A is the structure in dotted box, and B is the other parts. The transition t4 is the only portal transition between A and B. From the viewpoint of A through t4, A does not know the inner structure and inner behavior of B, only two informations are observable: how many times t4 will be fired and the time range for each firing occurrence of t4.
B
We provide these informations based on the real-time property verification
method presented in the previous section. t4 is fired infinitely. The time ranges
for each firing occurrence are shown in Table 1. For each firing occurrence n
(n 2 N) of t4, the time range [tnmin, tnmax] is [5 + 17(n 1), 10 + 69(n 1)].
The behavior regularity in this case is that, except the first occurrence, the time
difference between current occurrence and the previous one is always in [
A sub-net B0 conforming to this regular pattern is constructed to replace original sub-net B, as shown in Fig. 2. Sub-net A is kept as before. The reachability graph of the reduced TPN only contains 3 states and 3 transitions, but exhibits the same real-time behavior as before from the viewpoint of A.
To summarize the main objective of this work from the above example, we aim to find the regularity of the real-time behavior for the TPN sub-nets from the viewpoint of observations. As we only observe TPN transitions, the real-time behavior from the viewpoint of observed transitions concerns both the firing occurrence times and the time range of each firing occurrence. A reducible subnet must be independent of its surrounding behavioral context. It means that Occurrence
Time [timin, timax]
Time Diff [timin timi1n, timax tima1x] whether it is "knocked out" from the system or not, it will exhibit exactly the same behavior whenever it is measured, in terms of occurrence times of the portal transition and its time range of each firing occurrence.
An overview of the approach is illustrated in Fig. 3. First, some reducible sub-nets like A, B, and C are identified from the whole TPN model using the Identification functions. These sub-nets contain either none incoming transition and one unique outgoing transition such as A, denoted as one-way-out pattern; or one incoming and one outgoing transitions such as B and C, denoted as generic pattern. The regularity of real-time behaviors for each reducible sub-nets A, B and C are searched using Reduction functions relying on observer-based property verification method. If the regularity is founded, reduced sub-nets (A0, B0, and C0) are constructed to replace the original ones after their soundness is assessed by the Refinement functions, which also rely on the observer-based property verification method. As the one-way-out pattern and the generic pattern rely on different identification functions but similar reduction and refinement functions, for the page limit, we only develop our discussion based on the one-way-out pattern. 5
The regularity of real-time behavior depends on the characteristics of a system. Fig. 4 illustrates two possible regularities of real-time behavior from the viewpoint of observed transitions. The TPN in Fig.4 (a) has 3 sub-nets: A, B and C. A (resp. B) has a unique portal transition TA (resp. TB) to C, and produces tokens via TA (resp. TB) periodically or sporadically. From the viewpoint of C,
System A
A'
B
B'
C'
C regardless the complex inner behaviors of the A and B, they can be seen as single transitions that may fire regularly under a pattern to feed C by tokens. There exists thus an opportunity to abstract and redefine this regularity to a reduced TPN A0 (resp. B0) that may contains less states and transitions than the original one.
A TA B TB (a)
C
A' [t!,t"] [t#,t$] [tm,tn] ….
C (b)
B' ….
[ti,tj] [tp,tq] [tx,ty]
When the observation is performed on a TPN transition, the regularity of its firing occurrence is either finite or infinite. The time range of each firing occurrence can be measured using observers if the time ranges are bounded.
Fig. 4 (b) shows two kinds of possible regularity. Assume that we observe the firing time of transitions TA and TB for each firing occurrence. The occurrence of TA/TB can be either finite (A) or infinite (B). An infinity observer can be added on a transition to check its infinity. Each occurrence Ti has a bounded time range [timin, timax]. These ranges are derived by adding BCET (Best Case Execution Time) and WCET (Worst Case Execution Time) observers on TA and TB.
Finite Firing Occurrence If the occurrence is finite, the sub-net A can be represented by a finite sequential section of transitions Tseq = {Ti} (i 2 N) with adapted time range [Ti.min, Ti.max], where Ti.min = timin timi1n, and Ti.max = timax tima1x and t0min = t0max = 0. It is possible that the regularity of A contains several control modes that lead to several branches with finite sequential transitions.
Infinite Firing Occurrence If the occurrence is infinite, as we focus on finitestate systems, the states in sub-net B must be finite. In other words, there must exist a repeating pattern in B. Depending on system’s behavior, there are several possible repeating patterns, such as single loop pattern, nested loop pattern, etc. In this paper, we only discuss one of them: the pattern that is composed of an eventual finite sequential section of transitions Tseq = {Ti} (i 2 N) and a loop section of transitions Tloop = {Tj } (j 2 N). The other patterns are under study. Therefore, for now, if the system does not behave the infinite regularity with an eventual sequential section and a loop section, it is considered as non-reducible. 6
Real-Time Property Specific Reduction
The property specific state space reduction method follows three steps
(functions): identification, reduction and refinement, which rely on the real-time
property specification and observer-based verification approaches presented in [
Identification Function for One-Way-Out Pattern We first define a symbolic system to ease the discussion: – t+ and t : for a given transition t, represent respectively the outgoing and incoming arcs of t. – p+ and p : for a given place p, represent respectively the outgoing and incoming arcs of p. – TR(N) and PR(N): for a given TPN N , represent respectively the sets of reducible transitions and places.
We distinguish the reducible and non-reducible TPN structure. Non-reducible elements include those structures directly associated with properties, including observer structures, structures directly linked to observers and places/transitions referred to by reachability assertions. The other parts are considered as reducible.
Before performing property specific reduction, some property-irrelevant structures can be directly removed from the reducible net. They are the structures that have causality to the observers. The exact causality can be measured using the reachability graph of the whole system. The paradox exists here: if the whole reachability graph can be generated, we may not need any reduction method. Therefore, to ensure the safety of the removal, we rely on the dependency analysis in TPN as a over-approximation. The detailed dependency algorithm is trivial thus will not be presented here. Now assume the set of TR(N) and PR(N) are available after the removal. Identification function F(N ) = <A, Tout> identifies, for a given TPN N , the enclosed sub-net A that could be possibly reduced (necessary condition), and the unique portal outgoing transition Tout: – A is a connected graph, A ⇢ N , Tout 2 A – 8 p 2 A, (p 2 PR(N)) ^ (p+ ⇢ A) ^ (p ⇢ A) – 8 t 2 A, (t 2 TR(N)) ^ (t ⇢ A) – (Tout 2 A) ^ (To+ut \ A 6= ; ) 6.2
Reduction Function Reduction function G(A, t) = <NS, NL> extracts, for a given sub-net A and the outgoing portal transition t, the behavioral equivalent sequential section NS for the finite cases, or an eventual sequential section NS and the loop section NL for the infinite cases. It first checks the infinity of t in sub-net A using an infinity observer. In both cases, the bounding time range [timin, timax] is measured using predefined BCET and WCET observers for the ith firing occurrence of t. Building Sequential Section In the finite case, there is only a sequential section NS. The set of sequential transitions Tseq = {Ti} (i 2 N) in NS is built using [timin, timax]. Each transition Ti in Tseq is associated with a time range [Ti.min, Ti.max]. The algorithm for building NS from A using the transition t is described in Algo. 1. Initially, tomin and t0max are set as 0. NS starts from an initial place with one token. Whether ti has occurred is checked using tHasOcc(i) function relying on an occurrence observer. For each occurrence (i) of fired t, a pair of BCET and WCET observers are added to t in the sub-net A to compute the timin and timax. Then the time range [Ti.min, Ti.max] is associated to the transition Ti. Ti is added in NS, and an associated new place without token is also added in NS.
Data: A, t Result: NS tomin := 0, t0max := 0 ; NS.add(new Place(1)) ; i := o ; while tHasOcc(i++) do timin := getOccBCET(A,t,i) ; timax := getOccWCET(A,t,i) ; Ti.min = timin timi1n ; Ti.max = timax tima1x ;
NS.add(Ti, new Place(0)) ; end
Building Loop Section In the infinite case, the key issue is to identify the firing occurrence of t that divides the sequential section NS and the loop section NL. The Algo. 2 is proposed to build the NS and NL sections by searching for the loop starting transition (loopStartIndex) and the length of loop (loopLength).
Data: A, t, occT hreshold, loopT hreshold Result: NS, NL t0min := 0, t0max := 0 ; NS.add(new Place(1)) ; occ := 0 ; while occ++ occThreshold do tomcicn := getOccBCET(A,t,occ); tomcacx := getOccWCET(A,t,occ) ; for loopStartIndex = 0; loopStartIndex < occ; loopStartIndex ++ do for loopLength = 1; loopLength occ - loopStartIndex; loopLength ++ do match : = 0 ; for index = loopStartIndex; index occ - loopLength; index++ do if isSame(<timnidnex, timnadxex>, <timnidnex+loopLength, tindex+looplength>) then
max match++ ; end else break; end if match loopThreshold then for k = 1; k < loopStartIndex; k++ do
Tk.min = tkmin tkmin1; Tk.max = tkmax NS.add(Tk, new Place(0)) ; tkma1x ; end for k = loopStartIndex; k < loopStartIndex + loopLength; k++ do
Tk.min = tkmin tkmin1; Tk.max = tkmax NL.add(Tk, new Place(0)) ; NL.connect(lastPlace, TloopStartIndex) ; tkma1x ; end return ; end end end end
As the firing occurrence of t is infinite, an occurrence bound value is predefined as occT hreshold to stop the algorithm. As the Identification function F(N ) uses necessary conditions, the identified sub-net A is considered as nonreducible if the loop section cannot be found using occT hreshold. Another bound value loopT hreshold judges whether the loopStartIndex and the loopLength are found. If the loop pattern holds for loopT hreshold times, it is considered that this division of NS and NL is statistically correct. It is obvious that no matter how big the loopT hreshold is, the assurance cannot reach 100%, because the loop execution is infinite. In order to make sure that the reduced net refines exactly the same behavior as before, a pre-check (refinement function) must be performed before accepting the reduced structure. 6.3
Refinement Function The refinement function verifies the behavioral equivalence between the reduced sub-net and the original one. Fig. 5 shows the principle of this function: comparing the time range of each firing occurrence between the nets B and B0. It is realized by adding time interval observers between the transition TB in B and the transitions Ti in B0. Although the firing occurrence is infinite, under the repeating pattern, the number of Ti is finite. If the refinement fails, it means the system does not fit the behavior regularity, and thus the reduction method cannot be applied.
B
TB occ1 occ2 occi observer check ….
[ti,tj]
T1 [tp,tq] T2 [tx,ty] Ti
B'
It is possible that the observed time range do not fully refine the original
behavior because of possible "time holes" in this range. For example, a transition
can fire during [
For a given observed range [min, max] of transition T , at its ith occurrence, the assertion checkk "exist Ti between k and k+1 " will be checked for all min k < max. If checkk. If the check does not pass, the time range will be broken into two sections: [min, k] and [k+1,max]. To be more general, if checkk1 , checkk2 , ... checkkn do not pass, the final refined equivalent time ranges of this occurrence will become [min, k1], [k1 + 1, k2], ..., [kn + 1, max]. Accordingly, the sequential transition of the equivalent sub-net will be refined to a sub-structure which contains branches representing all possible firing time range after removing those impossible ranges. An example in Fig. 6 (a) shows that the transition T in the reduced sub-net A exhibits a firing time range [t3, t4]. But there exists time holes on this time range, and thus the real time behavior is [t3, t03] [ [t04, t4], where t03 < t04. The transition T should be replaced by the sub-range structure (grey part in Fig. 6 (b)).
A [t!,t"] [t#,t$]
T …. [tm,tn] (a)
C
C A' [0,0] [t#,t#'] [t!,t"] [0,0] [t$',t$] ….
[tm,tn]
(b)
To experiment the property specific reduction method, we use an avionic case
study investigated by M. Lauer et al. [
The latency requirement is assessed in the case study. It depends on the functional chain in Fig. 7. At any time, the pilot can request some information on a given waypoint. The KU1 (Keyboard and Cursor Control Unit ) controls the physical device used by the pilot to enter his requests. When KU1 receives a request (req1), it broadcasts wpid1 and wpid2 to the Flight Managers FM1 and FM2 respectively. The FMs manage the flight plan, i.e., the trajectory between successive waypoints. When a request occurs, both query the NDB (Navigation Database) by sending query1 (resp. query2) to retrieve the static information on the waypoint such as the latitude and the longitude. The NDB separately answers each FM by sending a message answer1 (resp. answer2) containing the expected data. Upon reception of this message, each FM computes two complementary dynamic data: the distance to the waypoint, and the ETA (Estimated Time of Arrival ). These data (wpInf o1 and wpInf o2 resp.) are periodically sent to respective MFDs (Multi Functional Display) which periodically elaborate the pages to be displayed on the screens. The KU1, FMs, NDB , MFDs are asynchronous functional modules.
req1
KU1 wpId1 wpId2
FM1 FM2 query1 query2
NDB NDB answer1 answer2
FM1 FM2 wpInfo1 wpInfo2
MFD1 MFD2 disp1 disp2
The latency requirement guarantees that the system responds quick enough to a request. It corresponds to the time elapsed between pilot’s request (req1) and the first occurrence of the display signal depending on req1 (disp1). Therefore, the real-time property here is the worst case time (WCT) and best case time (BCT) between req1 and the first occurrence of disp1 depending on req1.
We model the functional chain in TPN. The WCT and BCT observers are added respectively to the TPN. A binary search algorithm is used to search for the bound values. The computation results (verified under MacOS 10.6.8 with a processor 2.4 GHz Intel Core 2 Duo) are shown in Table 2. The WCT (resp. BCT) is 450.4 (reps. 75.2) ms. By applying the reduction approach, the state space is significantly reduced. Take the WCT for example, compared to the verification time 278.313 s before reduction, the verification time is reduced to 2.484 s. answerP NDB!P 1 answerP 1 !... answer2 ND!B1 answer1 FM! 1 wpInfo1 MFD!1 disp1
Before apply this reduction method, the state space begins to explode even the NDB number is 2 under the test environment. By increasing P from 1 to 11, we give out the state/transition number, reduction time, model checking (MC) time and solving time after applying the reduction method in Table 3. The reduction result is prominent. The solving time is almost linear with respect to the system’s scale. This case study shows that after reduction, the explosive systems can be analyzed, if the systems conform to the behavioral regularities. This method turns the combination problem of O(N · M ) into a divide-andconquer problem of O(tiden + n · N + M · N 0), where – N is the state unfolding complexity of the target sub-net, – M is the complexity of the other parts of the TPN, – N 0 is the state unfolding complexity of the reduced sub-net, 1 N 0 N .
It is expected that 1 N 0 ⌧ N if the system conforms to the behavioral regularity. – tiden is the time for identification, it is O(NS2), where NS is the number of places and transitions in the TPN system. – n is unfolding times of A by the reduction, refinement and cavity detection • Finite case reduction: 2NB4 · Aobs, NB is the defined bound value of occurrence times, Aobs is the unfolding time of A with observer. • Infinite case reduction: 2NB4 · Aobs, NB is the defined bound value of occurrence times. • Refinement: (nS + nL) · Aobs, nS is the length of sequential section, nL is the length of loop section.
nSP+nL
i=1 • Cavity Detection: (maxi mini) · Aobs
This method relies on the observers, it may thus take time to search for the bound values of time ranges. In some cases, if the system does not conform to the behavioral regularity, it can only be known after performing the reduction and refinement methods. As our purpose is to reduce the state space of model checking, the trade-off between computation time and the state space is acceptable, except that the computation time is out of the predefined thread-hold value. This is then an engineering problem. 9
This paper proposes a real-time property specific reduction approach for TPN based model checking. We illustrate the reduction method for the one-way-out pattern. More generic pattern with one incoming portal transition and one outgoing transition uses different identification function, but similar reduction and refinement functions. This method makes the verification more scalable for systems conforming to some behavioral regularities. It makes a trade-off between the state space and the solving time, and allows to verify large scale systems that will easily encounter combinatorial explosion problem, especially for the asynchronous real-time systems. The case study shows that after reduction, the explosive systems can be analyzed, if the systems conform to the behavioral regularities. The reduction and refinement functions rely on the real-time property specification and observer-based verification approaches. For now, we have defined two behavioral regularities for the finite and infinite firing occurrence, and provided reduction methods for the pattern with an eventual sequential section and a loop section. Other real-time behavioral regularities are under study. Similar approaches can be studied to reduce the state space for verifying other families of properties.
This work was funded by the FUI P and OpenETCS projects. We also wish to thank Michaël Lauer and Frédéric Boniol for the sharing of the avionic case study.