Interrupt-Driven System Verification Method Based on Interrupt Sequence Diagram

Abstract

An interrupt-driven system verification method based on interrupt sequence diagrams includes the steps of: establishing an interrupt-driven system model based on an interrupt sequence diagram, dividing interaction fragments in the obtained interrupt sequence diagram into basic interaction fragments and composite interaction fragments and sequentially converting the basic interaction fragments and the composite interaction fragments into the corresponding automaton models, combining the automaton models into one automaton model, adding the constraints in the interrupt sequence diagram to the converted automaton model, adding the verification attribute information as a constraint to the converted automaton model, describing an automaton as an input format acceptable to the automaton verification tool, and verifying the model with the automaton verification tool.

Claims

1. An interrupt-driven system verification method based on an interrupt sequence diagram, characterized by comprising the steps of: Step 1, establishing an interrupt-driven system model based on an interrupt sequence diagram, wherein the interrupt sequence diagram is comprised of interaction objects, interaction fragments, constraints and verification attributes; providing that an interaction event within interrupt combined fragments and an event outside the interrupt combined fragments have no temporal partially-ordered relation because when interrupts may happen and get processed are uncertain; in terms of a priority of the interrupts, providing that execution of an interrupt fragment with a high priority can break execution of an interrupt with a low priority, but the execution of the interrupt with the low priority cannot break the execution of the interrupt with the high priority; in terms of a conditional expression, providing that if the conditional expression is true, then a interrupt task can be triggered, otherwise, the interrupt task cannot be triggered; Step 2, dividing the interaction fragments in the interrupt sequence diagram obtained in step 1 into basic interaction fragments and composite interaction fragments; Step 3, sequentially converting the basic interaction fragments and the composite interaction fragments into corresponding automaton models; Step 4, combining the automaton models obtained in step 3 into one automaton model, whereby a converted automaton model from the interrupt-driven model is obtained; Step 5, extracting the constraints in the interrupt sequence diagram, and adding the constraints to the converted automaton model; Step 6, extracting the verification attribute in the interrupt sequence diagram, and adding the verification attribute as a constraint to the converted automaton model; Step 7, describing an automaton as an input format acceptable to an automaton verification tool; and Step 8, verifying with the automaton verification tool.

2. The interrupt-driven system verification method based on the interrupt sequence diagrams according to claim 1, characterized in that: the interrupt sequence diagram in step 1 is a two-dimensional diagram; the interaction objects are listed along the horizontal axis sequentially; the vertical axis indicates time increasing vertically downwards and is used for describing a time sequence of the interaction objects; the interaction objects are represented as lifelines, and the interaction among the objects is described as messages; the message is a communication mechanism among objects wherein a sending object sends a signal to another receiving object or several other receiving objects, an arrow is used for describing a transmission process of the message, a name of the message is marked above and below a line with the arrow, and sending and receiving events of the message have unique event names marked at a starting point and an ending point of the line with the arrow; a complex control flow in the interrupt sequence diagram is represented as combined fragments having their functions determined respectively by a type of interaction operations thereof, where “loop” represents a loop operation, “alt” represents an alternative operation, “opt” represents an optional operation, the same as in a UML sequence diagram; “int”, however, is an additional operation of the interrupt sequence diagram to the UML sequence diagram, where a boundary of the combined fragments is also represented as a box, at an upper left corner of which a character string “int” indicates that the type of the combined fragments is an interrupt operation, p indicates the priority of the interrupt, id is a name of the interrupt combined fragments, and “condition” is a conditional expression indicating a condition under which an interrupt occurs.

3. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that a method for converting the basic interaction fragments and the composite interaction fragments into corresponding automaton models in step 3 comprises the steps of: 1) for the basic interaction fragments, representing a basic interaction sequence as a quadruple BIS=(O, M, E, V), where O represents an interaction object set, M represents a message set, E represents an event set, and V represents a partial-ordered relationship among interaction events, obtaining a set T of traces of the interaction sequence on this basis, and then conducting conversion based on an algorithm, wherein: firstly, an initial state q0 is generated, a set L is a set of events that occur during a plurality of transitions from the state q0 to a state q, events without precursor events or with precursor events in the set L are found out in the set E-L to generate new transitions and states, and each set is updated to continue iteration until no new transitions and states are generated anymore; identical state nodes in the set L are merged in the process of generating the automaton, as a result, a simplest automaton is generated; and 2) for the composite interaction fragments, generating a corresponding automaton based on the interaction sequence therein according to the method of converting the basic interaction fragments, wherein q0 is an initial state and qn is a final state, and completion of the generation of the automaton depends on to different types of the combined fragments, which is implemented as follows: 21) for loop combined fragments, there has to be at least a times and at most b times of loops, at first, two new position nodes q and qf are generated, meanwhile, a control variable i is generated and keeps unchanged at any state node, and then a transition $q\stackrel{i<b,i:=i+1}{.fwdarw.}q0,q.fwdarw.\text{?}\mathrm{qi}$ $\text{?}\text{indicates text missing or illegible when filed}$ is generated, where a guard is used to limit the times of loops, and an assignment operation, i.e., i:=i+1, is used for recording how many times loops are executed and is incremented by 1 after each execution; $qn.fwdarw.\text{?}qi,qn.fwdarw.\text{?}q,$ $\text{?}\text{indicates text missing or illegible when filed}$ wherein a guard i≥a indicates that a state qf is open only after the loops are executed for times more than a, otherwise a transition back to state q takes place, and finally the position nodes q and qf are marked as new initial state and final state of the current automaton; 22) for optional combined fragments, to indicate whether a guard g is satisfied, a new position node q is first generated, and the new transitions $q.fwdarw.\text{?}q0\mathrm{and}q.fwdarw.\text{?}qn$ $\text{?}\text{indicates text missing or illegible when filed}$ are added, wherein the interaction within the combined interaction fragments is executed only when the guard g is satisfied, otherwise a direct switch to a final state qn takes place, and finally q is marked as a new initial state of the current automaton; 23) for alternative combined fragments, to indicate whether the guard g is satisfied, a new position node is first generated, a new transition from the state q to the initial state of the generated automaton is added, wherein the interaction within the interaction fragment is executed when the guard g is satisfied, otherwise the interaction within another interaction fragment is executed, and finally q is marked as a new initial state of the current automaton; 24) for the interrupt combined fragments, the interaction events in the interrupt combined fragments and the interaction events outside the fragments are provided to have no time sequence relationship, the interrupt combined fragments are treated as an independent subsystem, and a corresponding automaton is generated based on the interaction fragments therein.

4. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: a method of combining a plurality of automata generated in step 3 into one automaton in step 4 comprises the steps of: 1) combining all other interaction fragments except the interrupt combined fragments into one automaton, where the automatons corresponding to these interaction fragments are combined according to and because of relationships among the interaction fragments, and for the automata A and B, all the events corresponding to the automaton A occur prior to all the events in the automaton B; the steps of combining are as follows: 11) a final state qa of the automaton A is combined with an initial state lb of the automaton B, and a resulting state is marked as q; 12) any transition (l, e, qa) in the automaton A is changed to (l, e, q), wherein l is a state in the automaton A, and e is an event in the automaton A; and 13) any transition (lb, e′, l′) in the automaton B is changed to (q, e′, l′), wherein l′ is a state in the automaton B, and e′ is an event in the automaton B; and 2) combining an automaton model corresponding to the interrupt combined fragments into the automaton generated in step 1); a non-interrupt interaction fragment is regarded as an interaction fragment with a priority of 0, any other interrupt can break a task execution of the non-interrupt interaction fragment, and the steps of combining are as follows: 21) a high-priority automaton is connected into a low-priority automaton according to a principle that a high-priority task breaks a low-priority task; provided that the priority of automaton A is 1 and the priority of automaton B is 2, a state of the automaton B can occur after any state of automaton A; q is any state node of the automaton A, 10 is a initial state node of the automaton B, ln is an final state node of the automaton B, and the new transitions, i.e., $q\underset{\underset{\mathrm{gMacher}=\mathrm{mark};}{\mathrm{macher}=\mathrm{gMacher};}}{.fwdarw.}l0\mathrm{and}\ln \underset{\underset{\mathrm{gMacher}=\mathrm{macher};}{\mathrm{gMacher}=\mathrm{mark};}}{.fwdarw.}q$ are added, where “mark” is used for recording a unique mark when entering a current interrupt and exiting the interrupt, “gMacher” is a global variable and used for recording a mark when entering the current interrupt, and “macher” is used for recording a matching mark before entering the interrupt; the transition q.fwdarw.10 indicates that the matching mark before entering is stored by the macher when entering the high-priority automaton, the gMacher records the matching mark of the a current transition, the guard of the transition ln.fwdarw.q indicates that the transition to state q can be possible only when the matching marks are consistent, and the gMacher re-records the matching mark before entering the interrupt so as to be matched for use when exiting a prior interrupt; all the state nodes in the automaton A are subjected to the same operation to obtain a combined automaton C; and 22) all the automata are connected as described in step (21) according to the principle that the high-priority automaton breaks the low-priority automaton to obtain a combined automaton.

5. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: a method in step 5 of adding constraints to the automaton obtained in step 4 comprises the steps of: 1) generating a clock variable c for each common time constraint, and the clock variable c be capable of increasing in time at any state node; providing that the time constraint is e.sub.y−e.sub.x<a which indicates that event e.sub.y must be completed within a time units after event e.sub.x occurs; setting the clock variable c to be 0 for all event sequences when the event e.sub.x occurs, and adding a conversion guard c<a when the event e.sub.y occurs to indicate that the transition can happen and the automaton reaches a next state only when the condition is satisfied; and 2) generating a clock variable c for each project time constraint; indicating by a project time constraint (e.sub.y−e.sub.x)↑<a that the event e.sub.y must be completed within a time units after event e.sub.x occurs, the “a time units” excluding a running time of an interrupt task, wherein, at this time, the clock variable c increases in time at all the state nodes of the automaton where the events e.sub.y and e.sub.x are positioned, but remains unchanged at the other state nodes of the automaton; similarly, setting the clock variable c to be 0 for all event sequences when event e.sub.x occurs, pausing the clock when an interrupt occurs because a rate of change of the clock variable c at other state nodes is 0, restarting the clock when the interrupt task ends and a current task execution sequence is restored, and adding a transition guard c<a when event e.sub.y occurs to indicate that the transition can happen and the automaton reaches a next state only when the condition is satisfied.

6. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: a method in the step 6 of adding the verification attribute into the automaton obtained in step 4 comprises, getting a negation of the expressions describing a task timeout attribute and a data consistency attribute, and adding the negative expressions into the automaton as time constraint expressions according to the method described in step 5 into the automaton.

7. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: a method in step 7 of describing the automaton as an input format acceptable to the automaton verification tool comprises converting information of the automaton obtained in step 6 into a file format acceptable to the verification tool.

8. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: a method for generating automata corresponding to different interaction fragments in the interrupt sequence diagram are provided firstly, which can be applicable to the verification of the interrupt-driven system.

9. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 2, characterized in that: the interrupt sequence diagram is subjected to an overall analysis, the automata generated for different interaction fragments are combined into a complete automaton according to a strategy of combining in step 4, and constraints and the verification attribute are added into the automaton.

10. The interrupt-driven system verification method based on an interrupt sequence diagram according to claim 1, characterized in that: the interrupt sequence diagram model is converted into a corresponding automaton model, and the interrupt sequence diagram model is indirectly verified with the verification tool of the automaton model, helping developers with modeling and verification.

Description

BRIEF DESCRIPTION OF THE DRAWINGS

[0036] FIG. 1 is an interrupt sequence diagram according to an embodiment of the present invention.

[0037] FIG. 2 is an automaton model generated from basic interaction fragments according to an embodiment of the present invention.

[0038] FIG. 3 is an automaton model generated from loop combined interaction fragments according to an embodiment of the present invention.

[0039] FIG. 4 is an automaton model generated from interrupt combined interaction fragments according to an embodiment of the present invention.

[0040] FIG. 5 is an automaton model generated from all interaction fragments other than interrupts according to an embodiment of the present invention.

[0041] FIG. 6 is an automaton model with all interaction fragments combined according to an embodiment of the present invention.

[0042] FIG. 7 is an automaton model with a common time constraint added as a clock variable according to an embodiment of the present invention.

[0043] FIG. 8 is an automaton model with a project time constraint added as the clock variable according to an embodiment of the present invention.

[0044] FIG. 9 is an automaton model converted from the model of FIG. 1.

DETAILED DESCRIPTION OF THE INVENTION

[0045] The detailed process of model conversion and model verification using this method is described below in conjunction with a simple interrupt sequence diagram model.

[0046] A method for verifying an interrupt-driven system based on an interrupt sequence diagram in the embodiment is illustrated. 1) An interrupt sequence diagram model example introduced. This model is shown in FIG. 1, wherein: [0047] 11) Three interaction objects exist in the system: Agent, Service, and Peripheral objects. [0048] 12) Three combined interaction fragments exist in the system, including one loop combined fragment and two interrupt combined fragments IRQ 1 and IRQ 2, with priorities of 1 and 2, respectively. IRQ 1 is the interactions between the Agent and the Service, and IRQ 2 is the interactions between the Agent and the Peripheral. [0049] 13) Several constraints and verification attributes exist, including common time constraints and project time constraints. [0050] 2) The interaction fragments am divided into basic interaction fragments and combined interaction fragments according to step 2, and one basic interaction fragment and three combined interaction fragments (one loop combined interaction fragment and two interrupt combined interaction fragments) can be obtained as shown in FIG. 1. [0051] 3) All the obtained interaction fragments are converted into the corresponding automaton models, wherein: [0052] 31) A quadruple of the basic interaction fragment in FIG. 1 is represented as follows: an interaction object set O={Agent, Service, Peripheral}, a message set M={e12,e34}, an event set E={e1,e2,e3,e4}, and a timing relationship of interaction events V={e1<e2,e2<e3,e3<e4}, so we get a set of trace of the basic interaction fragment T={e1.fwdarw.e2.fwdarw.e3.fwdarw.e4}. Firstly, the initial position q0 of the automaton is generated according to the first line of the algorithm, and the automaton generated at this time has only one non-final state q0, without any transition. After entering the loop of the second line, L is an empty set, which means a set of events occurring from the initial state q0 to a position q through several transitions. In line 4, E-L=(e1,e2,e3,e4). In line 5, we find all events e that have no predecessor events and are not in the set L of events that have occurred; in line 6, the corresponding position and transition are generated, when the state set of the automaton is {q0,q1}, the transition set thereof is {(q0,e1, q1)}; after continuous iteration until there is no new state node and transition added to the automaton, a last state node is marked as the final node, and the automaton obtained is shown in FIG. 2. [0053] 32) An automaton is generated with reference to the method for the basic interaction fragment within the loop combined fragments in composite combined fragments, and then new state nodes q and qn are generated, new

[00005]$\mathrm{transitionsq}\stackrel{i<3,i:=i+1}{.fwdarw.}q0,q\stackrel{i\ge 3}{.fwdarw.}qn,q2\stackrel{i\ge 1}{.fwdarw.}\mathrm{qn}\mathrm{and}q2\stackrel{i<3}{.fwdarw.}q$

are added, after this, q and qn are taken as new initial and final states, respectively, and the resulting automaton is shown in FIG. 3. [0054] 33) For the interrupt combined fragments, since there is no timing relationship between the interrupt interaction fragments and the interaction fragments outside the interrupt, we regard the interrupt combined fragments as a separate subsystem, and the resulting automaton is shown in FIG. 4. [0055] 4) All the obtained automata are combined into one automaton, wherein: [0056] 41) All the automata except the automaton generated from the interrupt interaction fragments are combined into one automaton according to the time sequence relationship firstly, the final state of the automata with anteriority in the time sequence relationship and the initial state of the automata with posteriority in the time sequence relationship am combined, and state variables in relevant transitions are modified to obtain a new automaton as shown in FIG. 5; [0057] 42) The interaction fragment described by the automaton obtained in 41) is regarded as an interaction fragment with a priority of 0; because the automaton with a high priority can break the automaton with a low priority at any state node, it is necessary to connect the automaton with the high priority into the automaton with the low priority and add the transition of entering and exiting the automaton with the high priority at all state nodes with the low priority; as a an example, if the interrupt IRQ1 occurs in state q1, then we need to add two new transitions

[00006]$q1\underset{\underset{\mathrm{gMacher}=1;}{\mathrm{macher}=\mathrm{gMacher};}}{.fwdarw.}q8\mathrm{and}q10\underset{\underset{\mathrm{gMacher}=\mathrm{macher};}{\mathrm{gMacher}=1;}}{.fwdarw.}q1$

(q8 and q10 are the initial and final states, respectively, of the interrupt IRQ1), where gMacher is used for recording a unique matching mark of incoming and outgoing edges thereof, and macher is used for recording a matching mark before entering the high priority automaton; this is done for all other state nodes, and similarly for IRQ2, it should be noted that IRQ2 can break not only the basic interaction fragment, but also IRQ1. The resulting automaton model is shown in FIG. 6, where the guards and assignments of the transition am as follows: [0058] 1: macher=gMacher, gMacher:=0 [0059] 2: macher=gMacher, gMacher:=1 [0060] 3: macher=gMacher, gMacher:=2 [0061] 4: macher:=gMacher, gMacher:=3 [0062] 5: macher:=gMacher, gMacher:=4 [0063] 6: macher:=gMacher, gMacher:=5 [0064] 7: macher:=gMacher, gMacher:=6 [0065] 8: macher:=gMacher, gMacher:=7 [0066] 9: gMacher=0; gMacher:=macher [0067] 10: gMacher=1; gMacher:=macher [0068] 11: gMacher=2; gMacher:=macher [0069] 12: gMacher=3; gMacher:=macher [0070] 13: gMacher=4; gMacher:=macher [0071] 14: gMacher=5; gMacher:=macher [0072] 15: gMacher=6; gMacher:=macher [0073] 16: gMacher=7; gMacher:=macher [0074] 17: macher:=gMacher, gMacher:=0 [0075] 18: macher:=gMacher, gMacher:=1 [0076] 19: macher:=gMacher, gMacher:=2 [0077] 20: macher:=gMacher, gMacher:=3 [0078] 21: macher:=gMacher, gMacher:=4 [0079] 22: macher:=gMacher, gMacher:=5 [0080] 23: macher:=gMacher, gMacher:=6 [0081] 24: macher:=gMacher, gMacher:=7 [0082] 25: gMacher=0; gMacher:=macher [0083] 26: gMacher=1; gMacher:=macher [0084] 27: gMacher=2; gMacher:=macher [0085] 28: gMacher=3; gMacher:=macher [0086] 29: gMacher=4; gMacher:=macher [0087] 30: gMacher=5; gMacher:=macher [0088] 31: gMacher=6; gMacher:=macher [0089] 32: gMacher=7; gMacher:=macher [0090] 33: macher:=gMacher, gMacher:=0 [0091] 34: macher:=gMacher, gMacher:=1 [0092] 35: macher:=gMacher, gMacher=2 [0093] 36: gMacher=0; gMacher:=macher [0094] 37: gMacher=1; gMacher:=macher [0095] 38: gMacher=2; gMacher:=macher. [0096] 5) Constraints of the interrupt sequence diagram are extracted and added to the converted automaton model, wherein: [0097] 51) For the common time constraint expression, we take 2<e4-e3<4 as an example and set a clock variable c43, where a rate of change of the clock at all state nodes is 1; we find the transition where the event e3 occurs on the automaton model, initialize c43 to 0, add a guard 2<c43<4 to the transition where the event e4 occurs, which indicates that the next state node can be reached through this transition only if the clock variable satisfies the guard, and the automaton model of this part is shown in FIG. 7; and [0098] 52) For the project time constraint expression, we take 1<(e2-e1) ↑<2 as an example and set a clock variable c21, where a rate of change at all the state nodes of the automata where events e2 and e1 am occur is 1, and the rate of change at the state nodes of other automata is 0. Similarly, at the transition where event e1 occurs, c21 is initialized to 0, and the guard 1<e2-e1<2 is added to the transition where event e2 occurs, indicating that the next state node can be reached through the transition only when the clock variable satisfies the guard; in this regard, we take IRQ1 to break the messaging between events e2 and e1 as an example, and the automaton model is shown in FIG. 8. [0099] 6) Verification attribute information e2-e1<10 in the interrupt sequence diagram is extracted, we get the negation of the expression to obtain e2-e1>=10, which is added into an automaton model as a common time constraint, and a complete automaton model is finally generated, as shown in FIG. 9, wherein the guards and assignments of the transition are as follows: [0100] 1: macher:=gMacher, gMacher:=0 [0101] 2: macher:=gMacher, gMacher:=1 [0102] 3: macher:=gMacher, gMacher:=2 [0103] 4: macher:=gMacher, gMacher:=3 [0104] 5: macher:=gMacher, gMacher:=4 [0105] 6: macher:=gMacher, gMacher:=5 [0106] 7: macher:=gMacher, gMacher:=6 [0107] 8: macher:=gMacher, gMacher:=7 [0108] 9: gMacher=0; gMacher:=macher [0109] 10: gMacher=1; gMacher:=macher [0110] 11: gMacher=2; gMacher:=macher [0111] 12: gMacher=3; gMacher:=macher [0112] 13: gMacher=4; gMacher:=macher [0113] 14: gMacher=5; gMacher:=macher [0114] 15: gMacher=6; gMacher:=macher [0115] 16: gMacher=7; gMacher:=macher [0116] 17: macher:=gMacher, gMacher:=0 [0117] 18: macher:=gMacher, gMacher:=1 [0118] 19: macher:=gMacher, gMacher:=2 [0119] 20: macher:=gMacher, gMacher:=3 [0120] 21: macher:=gMacher, gMacher:=4 [0121] 22: macher:=gMacher, gMacher:=5 [0122] 23: macher:=gMacher, gMacher:=6 [0123] 24: macher:=gMacher, gMacher:=7 [0124] 25: gMacher=0; gMacher:=macher [0125] 26: gMacher=1; gMacher:=macher [0126] 27: gMacher=2; gMacher:=macher [0127] 28: gMacher=3; gMacher:=macher [0128] 29: gMacher=4; gMacher:=macher [0129] 30: gMacher=5; gMacher:=macher [0130] 31: gMacher=6; gMacher:=macher [0131] 32: gMacher=7; gMacher:=macher [0132] 33: macher=gMacher, gMacher:=0 [0133] 34: macher=gMacher, gMacher:=1 [0134] 35: macher=gMacher, gMacher:=2 [0135] 36: gMacher=0; gMacher:=macher [0136] 37: gMacher=1; gMacher:=macher [0137] 38: gMacher=2; gMacher:=macher. [0138] 7) The automaton is described as an input format acceptable to the automaton verification tool and verified in the automaton verification tool.

[0139] The foregoing is only a preferred embodiment of the present invention, and it should be noted that it will be apparent to those skilled in the art that various modifications and variations can be made in the present invention without departing from the spirit or scope of the invention.