Reliability analysis of CSP specifications using Petri nets

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

RELIABILITY ANALYSIS OF CSP SPECIFICATIONS USING

PETRI NETS AND MARKOV PROCESSES

Krishna M. Kavi, Frederick T. Sheldon, Behrooz Shirazi

University of Texas at Arlington

and

Ali R. Hurson

Pennsylvania State University

ABSTRACT

In our research we are developing methodologies andtools to permit stochastic analyses of CSP-based systemspecifications. In this regard, we have been developingmorphisms between CSP-based models and Petri net-basedstochastic models. This process has given us insight forfurther refinements to the original CSP specifications (i.e.,identify potential failure processes and recovery actions).In order to create systems that meet user needs in terms ofcost, functionality, performance and reliability, it isessential to relate the parameters needed for reliabilityanalysis to the user level specification.

Keywords: Formal specification, CSP, Petri Nets,Reliability analysis, Markov models.

1. INTRODUCTION

Computers are increasingly used in every day life intoday's society. These systems are monitoring andcontrolling complex and safety critical systems. It hasbeen conjectured that formal mathematically precisemethods should be used to design such systems. Amongthe benefits from using formal frameworks, we include[Ostroff 92]:

In the process of formalizing informalrequirements, ambiguities, omissions, andcontradictions will often be discovered.

A formal framework may lead to hierarchicalsemi-automated system development methods. A formal model can be verified for correctness bymathematical methods (rather than by exhaustivetesting).

A formally verified subsystem can beincorporated into a larger system with greaterconfidence that it will behave as specified.

Different designs can be evaluated and compared. A clear specification of interactions amongvarious subsystems may provide implementationinsights for avoiding performance pitfalls.

“When it comes to the implementation ofspecifications formally, one does not do it by writingprograms and then trying to prove that they meet thespecifications. Instead, one constructs correct programs insmall steps - each step taking the specification andproducing something that is bit closer to the finalprogram” [Hall 90]. At the other extreme, some formalspecification and verification methods strive for "fool-demonstration that one formal statement follows fromanother, and the validity of a statement depends on thevalidity of the statement from which it is http://plex systems are placed in environments that aredifficult to model accurately. Thus, it is not feasible (atleast not cost-effective) to prove the correctness of adesigned system in real environments. One must besatisfied by designing systems that will exhibit a highdegree of dependability. Thus, future systems will bedesigned to tolerate unpredictable conditions and operatesafely in the presence of hardware or software failures.

The research in formal specification and verification ofcomplex systems has often ignored the specification ofstochastic properties of the system. The normal practice isto derive designs and implementations of systems fromformal specifications. Designers concurrently developstochastic models of the target systems for the purpose ofreliability and performance analyses. While detailedanalyses require a clear understanding of theimplementation (hardware/software failure modes, failuredistributions, service distributions, workload, etc.), it isour belief that the cost of providing a desired level ofreliability and performance can be related to user levelspecifications, even if only in terms of upper and lowerbounds. It is also our belief that as specifications arerefined into detailed designs and actual implementations,the reliability and performance requirements can also berefined to reveal the trade-offs in design alternatives.

Stochastic Petri-nets have been used to analyzecomplex distributed processing systems in terms ofperformance and reliability. Numerous tools have beendeveloped for stochastic analysis of Petri nets (e.g., GSPN[Marsan 89], GreatSPN [Chiola 89], SPNP [Ciardo 89]).Petri nets however, are not very suitable for reasoningabout the functional correctness of a system.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

We have developed an initial set of rules for translatingCSP (Communicating Sequential Processes) specificationsinto Petri nets [Kavi 93]. In this paper we willdemonstrate, by using a simple example, (1) how CSPspecifications can be converted into Petri nets, (2) howPetri nets can be embellished with failure modes, (3) howthese failure modes can be converted into CSP processes sothat the feasibility of certain failure modes can be examinedby the user, and (4) how Petri nets can be analyzed forreliability (using user level information on failure rates).

2. FORMALISMS FOR SPECIFICATION

AND ANALYSISSince CSP and other specification models arecompositional, the usefulness of an analysis is improvedby partitioning large systems into smaller subsystemswhose reliability can then be approximated judiciously,giving greater comprehensibility and thereby reducing theanalysis complexity. It is hoped that the insights gainedwill lead to a set of tools for the specification of functionaland stochastic properties, as well as mechanical proofs andanalyses for correctness, reliability and performancemeasures.

2.1 Communicating Sequential Processes. TheCSP model was developed by Hoare and later extended byOlderog ([Hoare 85], [Olderog 86]). A program in CSPconsists of n > 1 communicating processes; this isnormally represented using the parallel compositionoperator (||), which is associative: P = {P1 || PP2 || .....||n}.

A process's actions are visible by means of itscommunications with other processes or the environment.The set of symbols representing the visible actionscomprise the alphabet (S) for the process. Processescommunicate synchronously by sending and receivingmessages: the sending and receiving actions (or events) areindicated using the input (?) and output (!) actions. Pi?x isthe action of receiving a value sent by process Pvariable x. Pi intoj! <expression> describes the action ofsending the value of the expression to Pj. Synchronizationis accomplished by using complementary input and outputcommands in the two communicating http://munication can be made selective by providing guards,where one of the alternative communication actions with asatisfied guard is selected. A guarded command has thegeneral syntax of the form <guard> → <command list>.A command list is a set of commands defining a sequenceof actions, alternative actions based on either deterministicor non-deterministic choice, recursive actions, or a STOPaction. Stop terminates (or deadlocks) a process. Thefollowing summarizes CSP syntax:P ::= STOP | (a → P) | (P\b) | (P

Q)

b Q) | (P; Q) | (µx P)

In CSP, capitalized names are used for process names,and lower case characters are used to denote visible actions.Here, (a → P) means, action 'a' followed by P, (P\b) is thesame as P except action b is hidden, (P

Q) represents a

represents a deterministic choice between P and Q, (PbQ)shows concurrent processes P and Q that synchronize onaction b, (P; Q) a sequence between P and Q, (µx P) isused for recursion.

example, a Rail-Road intersection is specified. The gatecloses when a train arrives at the intersection and remainsclosed until the train leaves the intersection. Although theproblem statement can be extended to handle multipletrains, only one train is specified here.

TRAIN = (IN_TRANSIT); (GATE ! a → AT_INTERSECTION); (GATE ! d → TRAIN)GATE =

(TRAIN ? a → CLOSE);

(TRAIN ? d → OPEN→ GATE)

RAIL_ROAD_CROSSING =

TRAIN {a,d} GATE

This specification shows two concurrent processes, theTRAIN and the GATE communicating via two activities,"a" and "d." The TRAIN outputs "a" (arriving) to theGATE as it approaches the intersection; proceeds throughthe intersection and outputs a "d" (departing) to the GATEas it leaves the intersection and continues to behave as aTRAIN. The GATE process receives an "a" from theTRAIN, closes the gate, waits for an input of "d" from theTRAIN before opening the gate and then behaves like aGATE. A few comments about the CSP specification arein order. The original CSP does not permit specificationof time with actions, although some recent extensions toCSP permit the association of time with actions. BecauseCSP uses point-to-point communication it is awkward todescribe the case where the GATE process accepts inputsfrom multiple TRAIN processes. Careful scrutiny reveals(AT_INTERSECTION) before the gate closes which leadsto unsafe behavior. Likewise, the train may depart whilethe gate is still closed which can be viewed as a fail-safebehavior. The Petri net equivalent reveals these flaws morereadily (see Figures 1 and 2).

2.2 Stochastic Petri Nets. The Petri net wasoriginally due to Carl Petri. In its simplest form, a Petrinet is a directed bipartite graph, where the two types ofnodes are known as places (shown as circles) andtransitions (shown as bars). Places normally represent

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

events while transitions represent actions. A transition isenabled if all its inputs contain at least one token (shownas dark circles inside places). Completion of the actiondefined by a transition causes a token to be assigned to eachof its output places. When a place is the input to morethan one transition, only one of the transitions is enabledbased on a non-deterministic choice. The state of a Petrinet is indicated by the number and location of tokens inplaces (known as a marking), and as transitions are enabled,the state of the Petri net moves from marking to marking.The complete set of markings of a Petri net can be obtainedusing reachability algorithms. When a Petri net isrestricted to contain at most one token in a place (or afinite number of tokens, say k), such a Petri net is knownas a safe net (or k-safe).

These initial concepts have been extended to permitprobabilistic choices on the outputs of a place, inhibitorarcs to transitions (i.e., a transition is enabled in theabsence of a token at its input place and such arcs canmodel zero testing), as well as the association of time anddistributions with either places or transitions. See [Murata89] for an excellent survey of Petri nets. We will rely onthe stochastic Petri nets that permit the association ofvarious probability distributions with transitions to modelperformance and reliability of the system. A stochasticPetri net (SPN) is a Petri net where each transition isassociated with a random variable that expresses the delayfrom the enabling to the firing of the transition. Whenmultiple transitions are enabled, the transition with aminimum delay fires first. When the random variable isexponential, the markings of the stochastic Petri net areisomorphic to the states of a finite Markov chain. Thetransition rate from state Mλi to Mj = qij is given by qλij =i1 + i2 + . . .+λ which takes the Petri net from marking Mim where λik is the delay in firing atransition tMki tofrom Mj (when more than one transition can cause the transitioni to Mj). The performance and reliability analysesof the system represented by the Petri net can be achievedby using an equivalent Markov process.

2.3 Mapping of CSP-Level Specifications intoPetri Nets. We have developed an initial set of rules fortranslating CSP specifications into Petri nets [Kavi 93].The translation relies on the fact that CSP specificationsare based on processes moving form one action to another.The activities which enable the actions of processes can bePetri net, while the actionsPetri nets. The translations between the CSP and Petri netmodels have not been formally verified to be isomorphic.However, we have developed rules which show theassociated Petri net structure for the majority of CSPprocess structures and compositions. The Petri netequivalent of a CSP specification need not be unique,because of the need to introduce dummy places ortransitions to maintain its bipartite nature. Intuitively, itis possible to reduce different Petri net equivalents into acanonical form. We plan to develop the necessary rules for

producing canonical Petri net representations of CSPspecifications.

Our goal is to demonstrate the feasibility of translatingbetween CSP and Petri nets so that stochastic propertiescan be specified at the CSP level, and analyzed usingstochastic Petri nets. Some example translations betweenCSP specifications and Petri nets are shown in theAppendix. Using these, we have converted the CSPexample of the Rail-Road Crossing.

The Rail-Road crossing presents a safetycritical system where two tasks that operate independentlymust communicate in order to coordinate closing the gatewhen the train nears the crossing. The gate must remainclosed until the train passes though. The Petri net isshown in Figure 1.

As stated earlier (¶2.1.1), a careful scrutiny reveals thatgate closes, exposing the system to unsafe behavior. Thispotential flaw becomes immediately visible from the Petrinet shown in Figure 1. If we assume that the gate alwaysopens and closes sooner than the time it takes the train toreach the crossing, the Petri net can be viewed as hazardfree.

Obviously some mechanism is needed to ensure thatthe train will not proceed unless the gate is closed. Oneway to redesign the system is to force the TRAIN processto wait until the GATE process completes CLOSEing thegate which will avoid such unsafe behavior. The Petri netof Figure 2 shows the additional synchronization (and itscorresponding CSP) that is necessary to ensure the systemwill operate in such a manner.

In Figure 2, a failure of the communication relatedactions may lead to a deadlock (the train will halt), butsynchronization between the TRAIN and GATE eliminatesthe possibility of trains passing through the intersectionun-guarded by an open gate. Failure to OPEN the gate isnot safety critical, yet should be avoided to preventcongestion of the associated infrastructure. It may bepossible to use Reward nets (and performability analyses)to associate a cost with such delays in opening of the gate.

3. SPECIFICATION OF STOCHASTIC

PROPERTIES

One of the major objectives of our research is toprovide assistance to the user in specifying not onlyfunctionality but also reliability, performance andexecution deadlines. In this paper we show how this isfacilitated by the translation of CSP specifications intoStochastic Petri nets. One important benefit, as we havealready shown, is how the Petri net (PN) equivalent of theRail-Road crossing elucidated the need for additionalsynchronization to avoid a safety-critical failure.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

Figure 1 Rail-Road Crossing with a Potential Hazard (unsafe PN Specification).

Figure 2 Rail-Road Crossing with a Hazard Eliminated.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

3.1 Failure Modes for the Rail-Road http://ing the Petri net of Figure 1, we will assume that alltransitions can fail. It should be noted however, that thePetri net of Figure 1 is unsafe, but for the purpose of theexample here, we assume the Petri net to be safe (i.e.,permit at most one token at a place). The Markings areshown in Figure 3. Note that Pidentified in the Petri net but are used to designate criticalCF and PNF are places notand non-critical failure events respectively.

Markings M firing of transitions (?a [t5 and M6 are critical markings resultingfrom slowbecause it is possible for the train to enter the intersection5]) and (Close [t6])before the gate has properly (or completely) closed.Similarly markings M11 and M12 occur due to a slowfiring of transitions (?d [t7]) and (Open [t8]) because it ispossible for the train to depart from the intersection and nothave the gate properly (or completely) open, although thesemarkings do not lead to a safety critical condition. Figure4 shows the Markov process based on the stochastic Petrinet. For analysis purposes, we will generally groupfailures into safety-critical (CF) and non-(safety-)critical(NF). A failure in sending or receiving the approaching("a") message and the closing of the gate are safety-critical.The CSP specification (and the corresponding Petri net) canbe augmented to show how such failures should be handled.For example, the communication failures can be handledusing time-out and re-transmit techniques. The failure ofthe gate closing action can be handled by sounding a loudalarm to alert pedestrians and traffic.

3.2 Stochastic Analysis. Using conventionaltechniques or stochastic Petri net tools (e.g., SPNP),discrete and continuous analyses can be performed. For thepurpose of this presentation, we have used Mathematica®to compute reliability of the rail-road crossing examplewith different failure rates (or probabilities) and servicerates (e.g., speed of the train, rate at which the gatemechanism operates). The values used in this paper (andhence the results of the analysis) are only for illustratingthe approach. It is not our intention to attach significanceto the failure rates, MTTFs obtained, or the probability ofdetected and undetected failures. These analyses are usefulin exploring different fault-handling mechanisms and thecost of providing fault tolerance. For example, moreelaborate fault-handling and fault-recovery mechanismscould be used to tolerate or prevent safety critical failures,while less attention may be paid to non-safety criticalfailures (see runs 2, 3, and 4 in Figures 5-6). Failure toopen the gate may anger people waiting at the crossing butsuch failures can be handled inexpensively by providing amechanism to manually open the gate. On the other hand,failure to close the gate is more severe, so traffic at thecrossing should be alerted reliably and automatically.probability assignments for our test runs of the Rail-Roadcrossing example. Table 2 shows the results of thestochastic analysis. In all runs we assume that the

mechanical failures have higher probabilities of failure thantransmission failures. In order to reduce the probability ofcritical failures, in runs 2, 3, and 4 we assume that fault-tolerant mechanisms are utilized to improve the gateclosing mechanism's reliability (as compared to the gateopening mechanism which is a non-critical failure) by thefactors of 100, 3, and 5 respectively. This achieved areduction in the probability of critical failures by thefactors of 17.5, 1.24, and 1.75. Such an analysis of theimprovements in the probability of critical failures can beused in deciding what level of fault tolerance is necessary.. The results of ourcontinuous analysis are shown in Figure 5. We have alsoinvestigated the trade-offs between the rate of train arrivals(µ1), the speed of the train (µ3), the rate of the gatemechanism (µ6, µ8) and the failure rates associated with thesignal transmission (λ2, λ4, λ, λ5, λfailures (gate mechanism, λ7) and the mechanical68). These results are shownin Table 2. Since we assume that signal transmissions aremore reliable than the gate's mechanical mechanism, wenotice that the reliability of signal transmission does notsignificantly impact the MTTF. Thus, the mechanicalfailures of the gate and the rate of gate closing (opening)are greater contributors to the reliability (or unreliability)of system. An interesting result of this analysis is thatwhen the train speed is such that it arrives at theintersection sooner than the gate has had time to close,then an improvement in the mechanical reliability will notimprove the system's reliability. This supports ourstatements about the need for additional synchronizationbetween the TRAIN and the GATE processes (Figure 2).

4. SUMMARY AND FUTURE WORK

Our objective in this paper is to show how CSPspecifications can be translated into Stochastic Petri netsfor the purpose of reliability and performance analyses.Such translations will give insight into the failure modes,and how fault handling mechanisms can be described as apart of the CSP specifications. We believe that ourapproach will provide the needed feedback to a designer sothat judicious cost-benefit analysis in providing fault-tolerance can be made. In this paper we have illustratedthis approach by using a simple example. The failureprobabilities used in the examples (hence the results of theanalysis) are for illustrating our approach, no othersignificance should be attached. Our only intention is toshow the complete process of specification and analysis.We hope to develop a tool for automatically translatingCSP specifications into Petri nets in order to use stochasticPetri net tools for the purpose of analysis.

Acknowledgments: Special thanks are extended toSherman Reed of the Electrical Engineering Department atUTA and Patrica Howell at NASA Langley ResearchCenter ofr their help with Mathematica®.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

Figure 3 Markings (M1 - 12) Based on the Hazardous Rail-Road Crossing PN Specification.

Figure 4 Markov Chain for Rail-Road crossing based on unsafe PN Specification.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

Table 1 Discrete Analysis: Probability Assignments

Table 2 Discrete Analysis: MTTF, Critical and Non-critical Failure Probabilities.µ1=0.0001; µ3=0.01

µ2=µ4=µ5=µ7 = 1λ2=λ4=λ5=λ7=0.00001µ6=µ8 =0.01λ6=λ8=0.001

System

Reliability

Time in Seconds

Figure 5 Continuous Analysis: System Reliability as a Function of Operational Time5. REFERENCES

[Chiola 89] G. Chiola. "A software package for the

analysis of generalized stochastic Petri net models,", Kyoto Japan, pp. 136-143,Dec. 1989.[Ciardo 89] G. Ciardo, J. Muppala and K.S. Trivedi.

"SPNP: Stochastic Petri Net Package," Kyoto Japan, pp. 142-151, Dec.1989.

[Hall 90] A. Hall. "Seven myths of formal methods," [Hoare 85] C.A.R. Hoare. , Prentice-Hall Int'l, Englewood Cliffs, NJ,1985.

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

[Kavi 93] K.M. Kavi, and B.P. Buckles. "Formal methods

for the specification and analysis of concurrentsystems" Tutorial Notes, Lake Charles, IL.,Aug. 20, 1993.[Marsan 89] M. A. Marsan, S. Donatelli and F. Neri.

"GSPN models of multiserver multiqueue systems,"1989.[Murata 89] T. Murata. "Petri nets: properties, analysis and

applications," , pp. 541-580,April 1989.

[Olderog 86] Olderog, E.R. LNCS-255,Springer Verlag, 1986.[Ostroff 92] Ostroff, J.S. "Formal methods for the

specification and design of real-time safety criticalsystems," 33-60, April 1992.[Trivedi 82] Trivedi, K.S., Prentice-Hall, Englewood, NJ, 1982.

TABLE 3 Continuous Analysis: Sensitivity Analysis Showing Service and Failure Rate Assignments

µ1 = 0.0001

λ2 = λ4 = λ5= λ7= 0.00001

µ= 0.01 ; µ= 0.01

λ= λ= 0.001 λ6 = λ8 = 0.0001 λ= λ= 0.0001

µ2= 0.01 ; µ6 = 0.001

λ6 = λ8 = 0.001 λ= λ= 0.0001 λ6 = λ8 = 0.0001

µ= 0.01 ; µ= 0.0001

λ= λ= 0.001 λ6 = λ8 = 0.0001 λ6 = λ8 = 0.0001

µ2= 0.001 ; µ6 = 0.01

λ6 = λ8 = 0.001 λ6 = λ8 = 0.0001 λ6 = λ8 = 0.0001

562252015156609664778642109121404260695606.

µ2= 0.001 ; µ6 = 0.0001µ= 0.0001 ; µ= 0.001

µ2= µ6= 0.001µ= 0.0001 ; µ= 0.01

MTTF

µ1 = 0.0001λ2 = λ4 = λ5= λ7= 0.00001 λ= λ= 0.001 λ6 = λ8 = 0.0001 λ= λ= 0.0001 λ6 = λ8 = 0.001 λ= λ= 0.0001 λ6 = λ8 = 0.0001

λ= λ= 0.001 λ6 = λ8 = 0.0001 λ6 = λ8 = 0.0001 λ6 = λ8 = 0.001 λ6 = λ8 = 0.0001 λ6 = λ8 = 0.0001

MTTF

10107101511054990026925654610993144021260211046

APPENDIX CSP TO PETRI NET TRANSLATIONS

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has g

a

b

STOPSTOP

a

b

(a→b→c)||{b} (d→b→e) b

a

b

a a→bµX.(b c→ X)

a

d

µX.(b→ X)

a

b

b b

b

c

c

e

d

((a→b){b} (c→b)) dτ

(a→b→c){b} (d→b→e))\ b) a d

from environment

(a

b)

from environment

µX.(a→ X a

b) b

a

b a b

a

c

τ

(a

b)||{a,b} (a

b)

a

b

b

c

e

a

b

b

P||{A} Q; P=µX.(a→X

b→X); Q=µY.(a→b→Y

c→Y); A={a,b}

a

b

a P Q b

c

P||{A} Q:

P||{A} Q:

c

a

orb

c

a

bhere bot h events b are equivalent

b