@MASTERSTHESIS{Yan07,
  title = {{Static Analysis of Stochastic Process Algebras}},
  author = {{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.},
  publisher = {Technical report},
  year = {2007},
  url = {http://rap.dsi.unifi.it/sensoriasite/mscthesis.pdf},
  address = {Informatics and Mathematical Modelling, Technical University},
  keywords = {Control Structure, Date Flow Analysis, Finite Automaton, PEPA, Stochastic Process Algebra},
  partner = {DTU, UEDIN},
  school = {Informatics and Mathematical Modelling, Tehnical University of Denmark},
  status = {public},
  task = {T3.4},
}