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.

…… 此处隐藏：23634字，全部文档内容请下载后查看。喜欢就下载吧 ……