Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Static Analysis of Stochastic Process Algebras
Fan Yang
abstract:
The Performance Evaluation Process Algebra, PEPA, is introduced by
Jane Hillston as a stochastic process algebra for modelling
distributed systems and especially suitable for performance
evaluation. A range of tools has already been developed that apply
this algebra to various application areas for different purposes.
In this thesis, we present a static analysis more precisely
approximating the control structure of processes expressed in
PEPA. The analysis technique we adopted is Data Flow Analysis which
is often associated with the efficient implementation of classical
imperative programming languages. We begin the analysis by defining
an appropriate transfer function, then with the classical worklist
algorithm we construct a finite automaton that captures
all possible interactions among processes. With the help of
the novel methodology of annotating label and layer to
the PEPA program, the approximating result is very precise.
Later we try to accelerate the analysis by two approaches, and
develop algorithms for validating the deadlock property of the PEPA
program. In addition, the thesis comes out with a tool that fully
implements the analyses and it could be used to verify the deadlock
property of the PEPA programs in a certain scale.
