nexoncn.com

文档资料共享网 文档搜索专家

文档资料共享网 文档搜索专家

当前位置：首页 >> >> Modeling and Verification of Safety-Critical Systems Using Safecharts

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

Pao-Ann Hsiung and Yen-Hung Lin

Department of Computer Science and Information Engineering, National Chung Cheng University, Chiayi, Taiwan?621, ROC hpa@computer.org

Abstract. With rapid development in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To make sure that safety-critical systems are really safe, there is need to verify them formally. However, the veri?cation of such systems is getting more and more dif?cult, because the designs are becoming very complex. To cope with high design complexity, currently model-driven architecture design is becoming a well-accepted trend. However, conventional methods of code testing and standards conformance do not ?t very well with such model-based approaches. To bridge this gap, we propose a model-based formal veri?cation technique for safety-critical systems. In this work, the model checking paradigm is applied to the Safecharts model which was used for modeling, but not yet used for veri?cation. Our contributions are ?ve folds. Firstly, the safety constraints in Safecharts are mapped to semantic equivalents in timed automata for veri?cation. Secondly, the theory for safety constraint veri?cation is proved and implemented in a compositional model checker (SGM). Thirdly, prioritized transitions are implemented in SGM to model the risk semantics in Safecharts. Fourthly, it is shown how the original Safecharts lacked synchronization semantics which could lead to safety hazards. A solution to this issue is also proposed. Finally, it is shown that prioritybased approach to mutual exclusion of resource usage in the original Safecharts is unsafe and corresponding solutions are proposed here. Application examples show the feasibility and bene?ts of the proposed model-driven veri?cation of safety-critical systems.

1 Introduction

Safety-critical systems are systems whose failure most probably results in the tragic loss of human life or damage to human property. There are numerous examples of these mishaps. The accident at the Three Mile Island nuclear power plant in Pennsylvania on 28th March, 1979 is just one unfortunate example. Moreover, as time goes on, there are more and more cars, airplanes, rapid transit systems, medical facilities, and consumer electronics, which are all safety-critical systems appearing in our daily lives. When some of them malfunction or fault, a tragedy is inevitable. The natural question that comes to mind is that can we use these systems without 100% warranty? Obviously,

F. Wang (Ed.): FORTE 2005, LNCS 3731, pp. 290–304, 2005. c IFIP International Federation for Information Processing 2005

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

291

the answer is negative. That’s why we need some methodology to exhaustively verify safety-critical systems. Traditional veri?cation methods such as simulation and testing can only prove the presence of faults and not their absence. Simulation and testing [11] both involve making experiments before deploying the system in the ?eld. While simulation is performed on an abstract model of a system, testing is performed on the actual product. In the case of hardware circuits, simulation is performed on the design of the circuit, whereas testing is performed on the fabricated circuit itself. In both cases, these methods typically inject signals at certain points in the system and observe the resulting signals at other points. For software, simulation and testing usually involve providing certain inputs and observing the corresponding outputs. These methods can be a cost-ef?cient way to ?nd many errors. However, checking all of the possible interactions and potential pitfalls using simulation and testing techniques is rarely possible. Conventionally, safety-critical systems are validated through standards conformance and code testing. Using such veri?cation methods for safety-critical systems cannot provide the desired 100% con?dence on system correctness. In contrast to the traditional veri?cation methods, formal veri?cation is exhaustive and provides 100% guarantee. Further, unlike simulation, formal veri?cation does not require any testbenches or stimuli for triggering a system. More precisely, formal veri?cation is a mathematical way of proving a system satis?es a set of properties. Formal veri?cation methods such model checking [4] are being taken seriously in the recent few years by several large hardware and software design companies such as Intel, IBM, Motorola, and Microsoft, which goes to show the importance and practicality of such methods for real-time embedded systems and SoC designs. For the above reasons, we will thus employ a widely popular formal veri?cation method called model checking for the veri?cation of safety-critical systems that are formally modeled. In the course of developing a model-based veri?cation method for safety-critical systems, several issues are encountered as detailed in the following. First and foremost, we need to decide how to model safety-critical systems. Our decision is to adopt Safecharts [4] as our models. Safecharts are a variant of Statecharts, especially for use in the speci?cation and the design of safety-critical systems. The objective of the model is to provide a sharper focus on safety issues and a systematic approach to deal with them. This is achieved in Safecharts by making a clear separation between functional and safety requirements. Other issues encountered in designing the formal veri?cation methodology for model-based safety-critical systems are as follows: 1. How to transform Safecharts into a semantically equivalent Extended Timed Automata (ETA) model that can be accepted by traditional model checkers? How can the transformation preserve the safety semantics in Safecharts? 2. What are the properties that must be speci?ed for model checking Safecharts? 3. Basic states in Safecharts have a risk relation with each other specifying the comparative risk/safety levels. How do we represent such information in ETA for model checking? 4. Safecharts have safety loopholes due to the lack of synchronization mechanisms. A motivational example will be given in Section 4.4.

292

P.-A. Hsiung and Y.-H. Lin

5. The current semantics of Safecharts states that mutual exclusion of resource usages can be achieved through priority. This is clearly insuf?cient as priorities cannot ensure mutual exclusion. The remaining portion is organized as follows. Section 2 describes the background form our model including a comparison between conventional validation, such as simulation and testing, and formal veri?cation. Basic de?nitions used in our work are given in Section 3. Section 4 will formulate each of our solutions to solving the above described problems in formally verifying safety-critical systems modelled by Safecharts. The article is concluded and future research directions are given in Section 6.

2 Related Work

A commonly-used method to demonstrate the safety of a system is proof by contradiction [13]. In this method, we assume that the unsafe states, identi?ed by hazard analysis, can be reached by executing the program. We then systematically analyze the code and show that the pre-conditions for a hazardous state are contradicted by the post-conditions of all program paths leading to that state. If this is the case, the initial assumption of an unsafe state is incorrect. If this is repeated for all identi?ed hazards, then the system is safe. However, to ?nd and list all possible hazards of safety-critical systems is dif?cult. For example, a system may fail due to an unpredicted hazard that may lead to a serious tragedy. This is not allowed, and that’s why we propose a more formal method to verify safety-critical systems that are modeled by Safecharts and veri?ed by model checking as introduced in the rest of this Section. Safecharts [4] is a variant of Statecharts intended exclusively for safety-critical systems design. With two separate representations for functional and safety requirements, Safecharts brings the distinctions and dependencies between them into sharper focus, helping both designers and auditors alike in modeling and reviewing safety features. Safecharts incorporates ways to represent equipment failures and failure handling mechanisms and uses a safety-oriented classi?cation of transitions and a safety-oriented scheme for resolving any unpredictable nondeterministic pattern of behavior. It achieves these through an explicit representation of risks posed by hazardous states by means of an ordering of states and a concept called risk band. Recognizing the possibility of gaps and inaccuracies in safety analysis, Safecharts do not permit transitions between states with unknown relative risk levels. However, in order to limit the number of transitions excluded in this manner, Safecharts provides a default interpretation for relative risk levels between states not covered by the risk ordering relation, requiring the designer to clarify the risk levels in the event of a disagreement and thus improving the risk assessment process. Timed Computation Tree Logic (TCTL) is a timed extension of the well-known temporal logic called Computation Tree Logic (CTL) which was proposed by Clarke and Emerson in 1981. We will use TCTL to specify system properties that are required to be satis?ed. Model checking [2,3,12] is a technique for verifying ?nite state concurrent systems. One bene?t of this restriction is that veri?cation can be performed automatically. The

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

293

procedure normally uses an exhaustive search of the state space of a system to determine if some speci?cation is true or not. Given suf?cient resources, the procedure will always terminate with a yes/no answer. Moreover, it can be implemented by algorithms with reasonable ef?ciency, which can be run on moderate-sized machines. The process of model checking includes three parts: modeling, speci?cation, and veri?cation. Modeling is to convert a design into a formalism accepted by a model checking tool. Before veri?cation, speci?cation, which is usually given in some logical formalism, is necessary to state the properties that the design must satisfy. The veri?cation is completely automated. However, in practice it often involves human assistance. One such manual activity is the analysis of the veri?cation results. In case of a negative result, the user is often provided with an error trace. This can be used as a counterexample for the checked property and can help the designer in tracking down where the error occurred. In this case, analyzing the error trace may require a modi?cation to the system and a reapplication of the model checking algorithm. Our safety-critical system model and its model checking procedures are implemented in the State-Graph Manipulators (SGM) model checker [14], which is a highlevel model checker for both real-time systems as well as systems-on-chip modeled by a set of timed automata.

3 System Model, Speci?cation, and Model Checking

Before going into the details of how Safecharts are used to model and verify safetycritical systems, some basic de?nitions and formalizations are required as given in this Section. Both Safecharts and their translated ETA models will be de?ned. TCTL and model checking will also be formally described. De?nition 1. Statechart Statecharts are a tuple F = (S, T , E, Θ, V, Φ), where S is a set of all states, T is a set of all possible transitions, E is a set of all events, Θ is the set of possible types of states in Statecharts, that is, Θ = {AN D, OR, BASIC}, V is a set of integer variables, and Φ ::= v ? c | Φ1 ∧ Φ2 | ?Φ1 , in which v ∈ V, ? ∈ {<, ≤, =, ≥, >}, c is an integer, and Φ1 and Φ2 are predicates. Let Fi be an arbitrary state in S. It has the general form: Fi = (θi , Ci , di , Ti , Ei , li ) where: – – – – – – θi : the type of the state Fi ; θi ∈ Θ. Ci : a ?nite set of direct substates of Fi , referred to as child states of Fi , Ci ? S. di : di ∈ Ci and is referred to as the default state of Fi . It applies only to OR states. Ti : a ?nite subset of T , referred to as explicitly speci?ed transitions in Fi . Ei : the ?nite set of events relevant to the speci?ed transitions in Ti ; Ei ? E. li : a function Ti → E × Φ × 2Ei , labelling each and every speci?ed transition in Ti with a triple, 2Ei denoting the set of all ?nite subsets of Ei .

Given a transition t ∈ T , its label is denoted by l(t) = (e, f cond, a), written conventionally as e[f cond]/a. e, f cond and a in the latter, denoted also as trg(t) =

294

P.-A. Hsiung and Y.-H. Lin

e, con(t) = f cond, and gen(t) = a, represent respectively the triggering event, the guarding condition and the set of generated actions. De?nition 2. Safechart Safecharts Z extend Statecharts by adding a safety-layer. States are extended with a risk ordering relation and transitions are extended with safety conditions. Given two comparable states s1 and s2 , a risk ordering relation speci?es their relative risk levels, s2 speci?es s1 is safer then s2 . Transition labels in Safecharts have an that is s1 extended form: e[f cond]/a[l, u)Ψ [G] where e, f cond, and a are the same as in Statecharts. The time interval [l, u) is a realtime constraint on a transition t and imposes the condition that t does not execute until at least l time units have elapsed since it most recently became enabled and must execute strictly within u time units. The expression Ψ [G] is a safety enforcement on the transition execution and is determined by the safety clause G. The safety clause G is a predicate, which speci?es the conditions under which a given transition t must, or must not, execute. Ψ is a binary valued constant, signifying one of the following enforcement values: – Prohibition enforcement value, denoted by . Given a transition label of the form [G], it signi?es that the transition is forbidden to execute as long as G holds. – Mandatory enforcement value, denoted by . Given a transition label of the form [l, u) [G], it indicates that whenever G holds the transition is forced to execute within the time interval [l, u), even in the absence of a triggering event. The Safecharts model is used for modeling safety-critical systems, however the model checker SGM can understand only a ?attened model called Extended Timed Automata [6] as de?ned in the following. De?nition 3. Mode Predicate Given a set C of clock variables and a set D of discrete variables, the syntax of a mode predicate η over C and D is de?ned as: η := false | x ? c | x ? y ? c | d ? c | η1 ∧ η2 | ?η1 , where x, y ∈ C, ? ∈ {≤, <, =, ≥, >},c ∈ N , d ∈ D, and η1 , η2 are mode predicates. Let B(C, D) be the set of all mode predicates over C and D. De?nition 4. Extended Timed Automaton An Extended Timed Automaton (ETA) is a tuple Ai = (Mi , m0 , Ci , Di , Li , χi , Ti , i ψi , τi , ρi ) such that: Mi is a ?nite set of modes, m0 ∈ Mi is the initial mode, Ci is i a set of clock variables, Di is a set of discrete variables, Li is a set of synchronization labels, and ∈ Li is a special label that represents asynchronous behavior (i.e. no need of synchronization), χi : Mi → B(Ci , Di ) is an invariance function that labels each mode with a condition true in that mode, Ti ? Mi × Mi is a set of transitions, λi : Ti → Li associates a synchronization label with a transition, τi : Ti → B(Ci , Di ) de?nes the transition triggering conditions, and ρi : Ti → 2Ci ∪(Di ×N ) is an assignment function that maps each transition to a set of assignments such as resetting some clock variables and setting some discrete variables to speci?c integer values.

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

295

A system state space is represented by a system state graph as de?ned in De?nition 5. De?nition 5. System State Graph Given a system S with n components modelled by Ai = (Mi , m0 , Ci , Di , Li , χi , Ti , i ψi , τi , ρi ), 1 ≤ i ≤ n, the system model is de?ned as a state graph represented by A1 × . . . × An = AS = (M, m0 , C, D, L, χ, T, ψ, τ, ρ), where: – M = M1 × M2 × . . . × Mn is a ?nite set of system modes, m = m1 .m2 . . . . .mn ∈ M, – m0 = m0 .m0 . . . . .m0 ∈ M is the initial system mode, 1 2 n – C = i Ci is the union of all sets of clock variables in the system, – D = i Di is the union of all sets of discrete variables in the system, – L = i Li is the union of all sets of synchronization labels in the system, – χ : M → B( i Ci , i Di ), χ(m) = ∧i χi (mi ), where m = m1 .m2 . . . . .mn ∈ M. – T ? M ×M is a set of system transitions which consists of two types of transitions: ? Asynchronous transitions: for each e ∈ T , ?i, 1 ≤ i ≤ n, ei ∈ Ti such that ei = e ? Synchronized transitions: ?i, j, 1 ≤ i = j ≤ n, ei ∈ Ti , ej ∈ Tj such that ψi (ei ) = (l, in), ψj (ej ) = (l, out), l ∈ Li ∩ Lj = ?, e ∈ T is synchronization of ei and ej with conjuncted triggering conditions and union of all transitions assignments (de?ned later in this de?nition) – ψ : T → L × {in, out} associates a synchronization label and a direction of communication with a transition, which represents a blocking signal that was synchronized, except for ∈ L, is a special label that represents asynchronous behavior (i.e. no need of synchronization), – τ : T → B( i Ci , i Di ), τ (e) = τi (ei ) for an asynchronous transition and τ (e) = τi (ei ) ∧ τj (ej ) for a synchronous transition, and – ρ : T → 2 i Ci ∪( i Di ×N ) , ρ(e) = ρi (ei ) for an asynchronous transition and ρ(e) = ρi (ei ) ∪ ρj (ej ) for a synchronous transition. De?nition 6. Safety-Critical System A safety-critical system is de?ned as a set of resource components and consumer components. Each component is modeled by one or more Safecharts. If a safety-critical system H has a set of resource components {R1 , R2 , . . . , Rm } and a set of consumer components {C1 , C2 , . . . , Cn }, H is modeled by {ZR1 , ZR2 , . . . , ZRm , ZC1 , ZC2 , . . . , ZCn }, where ZX is a Safechart model for component X. Safecharts ZRi and ZCj are transformed into corresponding ETA ARi and ACj , respectively. Therefore, H is semantically modeled by the state graph AR1 × . . . ×ARm ×AC1 × . . . ×ACn as de?ned in De?nition 5. For both hardware and software systems, a property or requirement can be speci?ed in some temporal logic. The SGM model checker chooses TCTL as its logical formalism, as de?ned below.

296

P.-A. Hsiung and Y.-H. Lin

De?nition 7. Timed Computation Tree Logic (TCTL) A timed computation tree logic formula has the following syntax: φ ::= η | EGφ | Eφ U?c φ | ?φ | φ ∨ φ , where η is a mode predicate, φ and φ are TCTL formulae, ? ∈ {<, ≤, =, ≥, >}, and c ∈ N . EGφ means there is a computation from the current state, along which φ is always true. Eφ U?c φ means there exists a computation from the current state, along which φ is true until φ becomes true, within the time constraint of ? c. Shorthands like EF, AF, AG, AU, ∧, and → can all be de?ned [5]. De?nition 8. Model Checking Given a Safechart Z that represents a safety-critical system and a TCTL formula, φ, expressing some desired speci?cation, model checking [2,3,12] veri?es if Z satis?es φ, denoted by Z |= φ. Model checking can be either explicit using a labeling algorithm or symbolic using a ?xpoint algorithm. Binary Decision Diagram (BDD) and Difference Bound Matrices (DBM) are data structures used for Boolean formulas and clock zones [3], respectively.

4 Model Checking Safecharts

Safecharts have been used to model safety-critical systems, but the models have never been veri?ed. In this work, we propose a method to verify safety-critical systems modelled by Safecharts. Our target model checker is State Graph Manipulators (SGM) [14,6], which is a high-level model checker for both real-time systems, as well as, Systems-on-Chip modelled by a set of extended timed automata. As mentioned in Section 1, there are several issues to be resolved in model checking Safecharts. Basically, a system designer models a safety-critical system using a set of Safecharts. After accepting the Safecharts, we transform them into ETA, while taking care of the safety characterizations in Safecharts, and then automatically generate properties corresponding to the safety constraints. The SGM model checker is enhanced with transition priority, synchronization, and urgency. Resource access mechanisms in Safecharts are also checked for satisfaction of modeling restrictions that prevent violation of mutual exclusion. Finally, we input the translated ETA to SGM to verify the safety-critical system satis?es functional and safety properties. Each of the issues encountered during implementation and the corresponding solutions are detailed in the rest of this section. 4.1 Flattening Safecharts and Safety Semantics Our primary goal is to model check Safecharts, a variant of Statecharts. However, Safecharts cannot be accepted as system model input by most model checkers, which can accept only ?at automata models such as the extended timed automata (ETA) accepted by SGM. As a result, the state hierarchy and concurrency in Safecharts must be transformed into semantically equivalent constructs in ETA. Further, besides the functional layer, Safecharts have an extra safety layer, which must be transformed into equivalent modeling constructs in ETA and speci?ed as properties for veri?cation.

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

297

There are three categories of states in Safechart: OR, AN D, and BASIC. An OR-state, or an AN D-state, consists generally of two or more substates. Being in an AN D-state means being in all of its substates simultaneously, while being in an ORstate means being in exactly one of its substates. A BASIC-state is translated into an ETA mode. The translations for OR-states and AN D-states are performed as described in [8]. Safety Semantics . The syntax for the triggering condition and action of a transition in Safecharts is: e[f cond]/a[l, u)Ψ [G], where e is the set of triggering events, f cond is the set of guard conditions, a is the set of broadcast events, [l, u) is the time interval specifying the time constraint, Ψ means the execution conditions for safety constraints, and G is the set of safety-layer’s guards. In Safecharts, e[f cond]/a appears in the functional layer, while [l, u)Ψ [G] may appear in the safety layer. The two layers of Safecharts can be integrated into one in ETA as described in the following. However, we need to design three different types of transitions [1]: – Eager Evaluation ( ) : Execute the action as soon as possible, i.e. as soon as a guard is enabled. Time cannot progress when a guard is enabled. – Delayable Evaluation (δ) : Can put off execution until the last moment the guard is true. So time cannot progress beyond a falling edge of guard. – Lazy Evaluation (λ) : You may or may not perform the action. The transition condition and assignment e[f cond]/a[l, u)Ψ [G] can be classi?ed into three types as follows: 1. e[f cond]/a There is no safety clause on a transition in Safechart, thus we can simply transform it to the one in ETA. We give the translated transition a lazy evaluation (λ). 2. e[f cond]/a [G] There is prohibition enforcement value on a transition t. It signi?es that the transition t is forbidden to execute as long as G holds. During translation, we combine them as e[f cond ∧ ?G]/a. We give the translated transition a lazy evaluation (λ). The transformation is shown in Fig. 1. 3. e[f cond]/a[l, u) [G] There is mandatory enforcement value on a transition t. Given a transition label of the form e[f cond]/a[l, u) [G], it signi?es that the transition is forced to execute within [l, u) whenever G holds. We translate functional and safety layers into a transition t1 and a path t2 , respectively. t1 represents e[f cond]/a, which means t1 is enabled if the triggering event e occurs and its functional conditional f cond is true. We give t1 a lazy evaluation (λ). Path t2 is combined by two transitions, t and tδ . Transition t is labeled [G]/timer := 0, where timer is a clock variable used for the time constraint, and we give t an eager evaluation ( ). When G holds, t executes as soon as possible, and t ’s destination is a newly added mode, named translator(t). tδ ’s source is translator(t), and its destination is t’s destination. tδ ’s guard is [timer ≥ l ∧ timer < u]. However, we give tδ a delayable evaluation (δ), which means it can put off execution until the last moment the guard is true. The procedure of translation is shown in Fig. 2.

298

P.-A. Hsiung and Y.-H. Lin

des(t) des(t)

src(t) src(t)

t ε : ([G] / timer := 0)

ε

t : (e[fcond] / a)

e[fcond]/a [G]

translator(t)

(e[fcond

G] /a)

e[fcond] / a [l,u) [G]

t δ : ( timer

l

timer

u)

δ

src(t)

src(t)

des(t)

des(t)

Fig. 1. Transformation of prohibition evaluation Fig. 2. Transformation of mandatory evaluation

4.2 Property Speci?cation for Safecharts In the safety-layer of Safecharts, there are two types of safety conditions on a transition, one is prohibition and the other is mandatory. After parsing the Safechart models of a safety-critical system, corresponding properties are automatically generated without requiring the user to specify again. Such properties are used to verify if the safety-layers work or not. As described in the following, to ensure that the safety constraints are working, two categories of properties are generated automatically for model checking. 1. AG((src(t) ∧ G) → ?EX(des(t))) If a transition t in Safechart has prohibition condition [G] in its safety-layer, it means that such transition is forbidden to execute as long as G holds. As shown in Fig. 1, t’s source is src(t), and its destination is des(t). Due to [G], src(t) is not allowed to translate to des(t) as long as G holds. If such property is tenable in our system state graph, which means that there is no transition from src(t) to des(t) executing whenever G holds, then we can know that the safety-critical system won’t become dangerous while G holds. 2. AG((src(t)∧G → ?EX(?translator(t))) and AG(translator(t)∧timer < u) If a transition t in Safechart has [l, u) [G] in its safety-layer, it means that such transition is enabled and forced to execute within [l, u) whenever G holds. As mentioned in former sections, we add two transitions for the safety-layer’s behavior, namely t and tδ , and a mode, translator(t) between them. From Fig. 2, when G holds, t must be executed as soon as possible due to its eager evaluation and the next active mode must be translator(t). Moreover, we know that if the mode translator(t) is active, then the next active state must be des(t) within the time limit timer ≥ l ∧ timer < u. If this constraint is violated, then the safety condition will not be satis?ed. 4.3 Transition Priority When modeling safety-critical systems, it is important to eliminate any non-deterministic behavior patterns of the system. Non-determinism arises if the triggering expressions of two transitions starting from a common state are simultaneously ful?lled. Because of its concern with safety-critical systems, Safecharts remove non-determinism in all cases except when there is no safety implication. In a Safechart model, a list of risk

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

Risk Band

299

6 t1 5 N t3 4 P

M t2 O

t4 t5 t6

3 t7 2 R t9 1

Q t8 S t10 T

Fig. 3. Risk graph with risk band

relation tuples is used to represent a risk graph [10]. Non-comparable conditions may still exist in a risk graph. An example [9] is given in Fig. 3, where, relative to other states, the state O may have received less attention in the risk assessment, resulting in it becoming non-comparable with other states in the graph, namely, the states N and P . Consequently, Safecharts do not allow any transition between them, for instance, a transition such as O P. As a solution to the above problem, the authors of Safecharts proposed risk band [9], which can be used to enumerate all states in a risk graph to make precise their relative risk relations that were not explicitly described. To adopt this method, we implemented transition priorities based on the risk bands of a transition’s source and destination modes. According to a list of risk relations, we can give modes different risk bands, as depicted in Fig. 3, where the maximum risk band, maxrb , is 6. We assign each transition a priority as follows: pri(t) = maxrb ? (rbsrc(t) ? rbdes(t) ), where pri(t) is the priority assigned to transition t, rbsrc(t) is the risk band of transition t’s source mode, and rbdes(t) is the risk band of transition t’s destination mode. Moreover, the smaller the value of pri(t) is, the higher is the priority of transition t. In Fig. 3, pri(t4) is 4, and pri(t6) is 3. Obviously, when t4 and t6 are both enabled, t6 will be executed in preference to t4. With risk bands, we can give a transition leading to a lower risk band state a higher priority. For implementing transition priorities into the SGM model checker, the triggering guards of a transition are modi?ed as follows [1]. τ (ti ) = τ (ti ) ∧

j≥i

?τ (tj ),

where τ (ti ) and τ (tj ) are the guard conditions of transitions ti and tj , j ≥ i means that tj ’s priority is higher than or equal to ti ’s, and τ (ti ) is the modi?ed guard condition of

300

P.-A. Hsiung and Y.-H. Lin

signal[i] signal[k]

signal[j]

route[x] route[y]

Fig. 4. Routes and signals

ti . This application results in allowing ti executed only if there is no enabled transition tj which has priority over ti . 4.4 Transition Urgency and Synchronization Safecharts have a safety/security loophole due to the lack of synchronization mechanisms. A motivation example is the railway signal system illustrated in Fig. 4, where a route can be requested, evaluated, and set when the required signals on a route are operating without faults and are in the free state. The Safecharts for route[x] and signal[i] are given in Fig. 5 and Fig. 6, respectively. A signal breaks down when either its lamp or its sensor fails. The signal mode is changed from OPR to FAULTY upon receiving either εl (lamp fail event) or εs (sensor fail event). However, this mode change is not synchronized with εl or with εs , thus in-between these two actions, a route could have been evaluated and set, although the signal is faulty which is not detected because the signal’s mode has not been changed as yet. Due to this lack of synchronization, safety loopholes exists in Safecharts. The route once set could allow a train to pass through a faulty signal endangering human lives as well as damaging properties. Safety-based resolution of non-determinism as proposed in [9,10,11] also does not solve this synchronization issue because non-determinism is resolved only among transition of the same Safechart and not among different Safecharts.

route[x]

SET

signal[i]

signal[i] in FREE signal[k] in FREE [signal[i] in FAULTY signal[k] in FAULTY] / allocate_i, allocate_k

MODE FAULTY LAMP L_OUT COLOR GREEN SENSOR S_OUT STATUS BUSY

Return_route[0,2] [signal[i] in FAULTY signal[k] in FAULTY] / release_i, release_k

?

?

ε

reject_route [signal[i] in FAULTY signal[k] in FAULTY]

?

?

request_route

ε

ε

/

ε

/

EVALUATE_REQ

OPR

L_IN

RED

S_IN

FREE

NOT_SET

Fig. 5. Safechart for route[x]

Fig. 6. Safechart for signal[i]

To solve the above problem, we propose the use of transition urgency as detailed in the following.

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts

301

route[x]

SET

Return_route[0,2] [signal[i] in FAULTY ∨ signal[k] in FAULTY] / release_i, release_k

signal[i] in FREE ∧ signal[k] in FREE ∧ regi=x ∧ regk=x [signal[i] in FAULTY ∨ signal[k] in FAULTY] / allocate_i, allocate_k

EVALUATE_REQ

NOT_SET

Fig. 7. Safechart for route[x] with mutual exclusion

Transition Urgency. As mentioned in Section 4.1, there are three types of transitions: eager evaluation ( ), delayable evaluation (δ), and lazy evaluation (λ). Transitions concerned with safety are given eager evaluation ( ) to ensure that when some malfunction or repair events happen, they can be executed ?rst to re?ect the correct status of a real-time system. In the railway signalling example, the model designer must give the transition with malfunctioning event ε an eager evaluation . As soon as the event ε occurs, the signal’s MODE is immediately changed to FAULTY. Thus route will not acquire the usage of signal, due to the safety-layer prohibiting guard condition signal[i] in FAULTY ∨ signal[k] in FAULTY. To eliminate the safety-loopholes in Safecharts and avoid errors due to the loopholes, the above method must be used to extend Safecharts. We have implemented the proposed method in our Safecharts veri?cation framework based on SGM. 4.5 Resource Access Mechanisms Safecharts model both consumers and resources. However, when resources must be used in a mutually exclusive manner, a model designer may easily violate the mutual exclusion restriction by simultaneous checking and discovery of free resources, followed by their concurrent usages. A motivation example can be observed in the railway signalling system as illustrated in Fig. 4, Fig. 5, and Fig. 6, where signal[k] must be shared in a mutually exclusive way between route[x] and route[y]. However, each route checks if signal[k] is free and ?nds it free, then both route will be SET, assuming all signals are fault-free. This is clearly a modeling trap that violates mutually exclusive usages of resources. A serious tragedy could happen in this application example as two intersecting routes are set resulting in perhaps a future train collision. From above we know that when consumers try to acquire resources that cannot be used concurrently, it is not safe to check only the status of resources. We need some kind of model-based mutual exclusion mechanism. A very simple policy would be like Fischer’s mutual exclusion protocol [7]. For each mutually exclusive resource, a variable is used to record the id of the consumer currently using the resource. Before the consumer uses the resource, it has to check if the variable is set to its id. Fig. 7 is a corrected vari-

≠

reject_route ∨ regi x ∨ regk [signal[i] in FAULTY ∨ signal[k] in FAULTY]

x

request_route / regi := x, regk := x

≠

302

P.-A. Hsiung and Y.-H. Lin

ant of the route Safechart from Fig. 5. When route[id] transits into EVALUATE REQ, it sets variable reg to its id. When route[x] tries to transit into the SET mode to acquire the usage of resource, it needs to check if reg is still its id. If reg is still x, then route[x] acquires the usage of the resource. Other mechanisms such as atomic test-and-set performed on a single asynchronous transition can also achieve mutual exclusion.

5 Application Examples

The proposed model-based veri?cation methodology for safety-critical systems was applied to several variants of the basic railway signaling system, which was illustrated in Fig. 4. The basic system was used to check the feasibility of the proposed methodology. The variants were used to check the scalability and ef?ciency of the methodology. The basic system consists of two routes: route[x] and route[y], where route[x] requires signal[i] and signal[k], and route[y] requires signal[j] and signal[k]. The numbers and sizes of the Safecharts and the generated ETA are given in Table 1. As illustrated in Figs. 8 and 9, for each route Safechart, one ETA is obtained and for each signal Safechart, ?ve ETA are generated. Thus, in the full system consisting of 5 Safecharts, 17 ETA are generated. It can be observed that the number of ETA modes, 40, is lesser than the number of Safecharts states, 56. The reason for this reduction is that hierarchical states do not exist in ETA. The synchronization and the mutual exclusion issues were both solved for this railway system as described in Sections 4.4 and 4.5, respectively.

SET pri = 1 pri = 1

FAULTY L_OUT

pri = 4

pri = 4

([signal[i] in FAULTY] / timer := 0, release_i, release_k)

([signal[k] in FAULTY] / timer := 0, release_i, release_k)

([(signal[i] in FREE) (signal[k] in FREE) (regi=x) (regk=x) ~(signal[i] in FAULTY)] / allocate_i, allocate_k)

([(signal[i] in FREE) (signal[k] in FREE) (regi=x) (regk=x) (signal[k] in FAULTY)] / allocate_i, allocate_k)

/ go_red

/ go_red

s

l

/ go_red

/ go_red

s

l

l

OPR

L_IN

pri = 1

SET_NOT_SET_translator

MODE ETA

LAMP ETA

(return_route)

(request_route)

pri = 2

pri = 2

pri = 2

([signal[k] in FAULTY] / timer := 0)

EVALUATE_REQ pri = 2

pri = 2

([signal[i] in FAULTY] / timer := 0)

GREEN

S_OUT

BUSY

release_i/ go_red

(reject_route)

([timer < 2])

go_green

([regk

([regi

EVALUATE_REQ_NOT_SET_translator

([timer < max])

RED

S_IN

FREE

COLOR ETA

SENSOR ETA

STATUS ETA

NOT_SET

Fig. 8. ETA for route[x]

Fig. 9. ETA for signal[i]

allocate_i

go_red

x])

x])

s

s

l

Modeling and Veri?cation of Safety-Critical Systems Using Safecharts Table 1. Results of the Railway Signaling System

303

Component Name # route 2 signal 3 full system 5

Safecharts # |S| |T | 1 4 4 1 16 10 5 56 38

ETA # |M | |T | 1 5 13 5 10 12 17 40 62

Table 2. Results of Application Examples

System |R| |S| A 2 3(1) B 2 4(1) C 2 4(2) D 3 4(1) E 3 5(2) F 4 5(1)

Safecharts # |S| |T | 5 56 38 6 72 48 6 72 48 7 76 52 8 92 62 9 96 66

ETA # |M | |T | 17 40 62 22 50 78 22 50 82 23 55 87 28 65 111 29 70 112

|φ| Issues Solved Time Mem Sync ME (?s) (MB) 16 3 1 230 0.12 19 4 1 292 0.12 22 4 2 337 0.13 24 4 1 326 0.14 33 5 2 515 0.14 32 5 1 634 0.14

|R|: total num of routes, |S|: total num of signals (num of shared signals), |φ|: num of properties generated. Sync: Num of synchronization issues solved, ME: Num of mutual exclusion issues solved

A number of variants of the basic railway signaling system were used for validating the proposed method’s scalability and ef?ciency. Varying the number of routes and the number of signals in each route increases the complexity and the concurrency of the system. However, we can observe from the veri?cation results in Table 2 that the amount of time and memory expended for veri?cation do not increase exponentially and are very well acceptable. The number of properties to be veri?ed also increase and thus their automatic generation is also a crucial step for successful and easily accessible veri?cation of safety critical systems. The number of issues solved imply how the proposed solutions in this work are signi?cant for the successful veri?cation of complex systems modeled by Safecharts.

6 Conclusions

Nowadays, safety-critical systems are becoming more and more pervasive in our daily lives. To reduce the probability of tragedy, we must have a formal and accurate methodology to verify if a safety-critical system is safe or not. We have proposed a formal method to verify safety-critical systems. Our methodology can be applied widely to safety-critical systems with a model-driven architecture. We hope our methodology can have some real contribution such as making the world a safer place along with the development of science and technology.

304

P.-A. Hsiung and Y.-H. Lin

References

1. K. Altisen, G. G¨ ssler, and J. Sifakis. Scheduler modeling based on the controller synthesis o paradigm. Real-Time Systems, 23:55–84, 2002. 2. E.M. Clarke and E.A. Emerson. Design and sythesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Logics of Programs Workshop, volume 131 of LNCS, pages 52–71. Springer Verlag, 1981. 3. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999. 4. H. Dammag and N. Nissanke. Safecharts for specifying and designing safety critical systems. In Proceedings of the 18th IEEE Symposium on Reliable Distributed Systems, pages 78–87, October 1999. 5. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for reattime systems. In Proceedings of the IEEE International Conference on Logics in Computer Science (LICS), pages 394–406, June 1992. 6. P.-A. Hsiung and F. Wang. A state-graph manipulator tool for real-time system speci?cation and veri?cation. In Proceedings of the 5th International Conference on Real-Time Computing Systems and Applications (RTCSA), October 1998. 7. K.G. Larsen, B. Steffen, and C. Weise. Fischer’s protocol revisited: A simple proof using model constraints. In Hybrid System III, volume 1066 of LNCS, pages 604–615, 1996. 8. L. Lavazza, editor. A methodology for formalising concepts underlying the DESS notation. ITEA, December 2001. 9. N. Nissanke and H. Dammag. Risk bands - a novel feature of Safecharts. In Proceedings of the 11th International Symposium on Software Reliability Engineering (ISSRE), pages 293–301, October 2000. 10. N. Nissanke and H. Dammag. Risk ordering of states in Safecharts. In Proceedings of the 19th International Conference on Computer Safety, Reliability, and Security, volume 1943 of LNCS, pages 395–405. Springer Verlag, October 2000. 11. N. Nissanke and H. Dammag. Design for safety in safecharts with risk ordering of states. Safety Science, 40(9):753–763, December 2002. 12. J.-P. Queille and J. Sifakis. Speci?cation and veri?cation of concurrent systems in CESAR. In Proceedings of the International Symposium on Programming, volume 137 of LNCS, pages 337–351. Springer Verlag, 1982. 13. I. Sommerville. Software Engineering. Addison Wesley, 6th edition, 2001. 14. F. Wang and P.-A. Hsiung. Ef?cient and user-friendly veri?cation. IEEE Transactions on Computers, 51(1):61–83, January 2002.

更多相关文档:

1 *Modeling* *and* *Verification* *of* Embedded *Systems* *using* Cadence SMV_专业资料。...For *safety-critical* applications an approach is needed to validate the ...

specification *and* *verification* *of* the main algorithm used for *safe* distributed...*of* development, veri cation, validation *and* test *of* *safety-critical* *systems*....

Stursberg *Verification* *of* PLC Programs given as Sequential Function *Charts* Abstract...industries to realize sequential procedures *and* to avoid *safety-critical* stat...

DATA-FLOW NETWORKS IN THE DESIGN *OF* *SAFETY-CRITICAL* *SYSTEMS*_专业资料。...*and* reasoning conducted *using* this *model*; formal *verification* *of* the *system*,...

UML-Based Software Architecture Descriptions *of* *Safety-Critical* *Systems*_专业资料...Effects *and* Criticality Analysis combined with Message Sequence *Charts* [6]. ...

This paper proposes a method *of* *using* the Term ...*verification* *of* interlocking *systems* scalability, *and*...*modeling* *and* *verification* *of* the *safety-critical* ...

Enterprise *modeling* in information *systems* planning ...accurate *verification* *of* the need to maintain the...will be displayed, *and* may also include *charts*....

Designing, Manufacturing, *and* Testing *Safe* Products...*Verification* Through Testing Testing alone is ...*of* techniques such as control *charts* *and* pre-...

16p. 1 Black *and* White Photograph, 3 *Charts*. ...*Modeling* *and* *verification* *of* a dual chamber implantable...Construction *and* Analysis *of* *Systems* - 18th Int....

machines Flow *charts* Natural language 6 ...*Modeling* *and* Coding Standards Checking *Model* *and* ...Complete *verification* process established Link to ...

5 Continuum *of* *System* *Verification* *and* Software ...*charts* *and* coverage hole analysis to aid ...This requires a *modeling* methodology that provides ...

scenarios, captured as message sequence *charts* (...Kramer, “Checking *Safety* Properties *Using* ...*Verification* *of* Web Service Compositions *and* ...

更多相关标签:

相关文档

- 1 Modeling and Verification of Embedded Systems using Cadence SMV
- Modeling and Verification of Embedded Systems using Cadence SMV
- Safety-critical systems, formal methods and standards
- Modeling and Automatic Failure Analysis of Safety-Critical Systems Using Extended Safechart
- PROBABILISTIC MODELING AND VERIFICATION OF LARGE SCALE SYSTEMS BY
- Design of safety-critical systems using the complementarities of success and failure domains with a
- Formal verification of safety-critical hybrid systems
- DESIGN METHODS OF SAFETY-CRITICAL SYSTEMS AND THEIR APPLICATION IN ELECTRONIC BRAKE SYSTEMS
- Facilitating the Maintenance of Safety-Critical Systems Using Formal Methods
- Modeling and Specification of Discrete Event Systems using Combined Process Algebra and

文档资料共享网 nexoncn.com
copyright ©right 2010-2020。

文档资料共享网内容来自网络，如有侵犯请联系客服。email:zhit325@126.com