Beta 1


Title Static Analysis of Stochastic Process Algebras
Author Yang, Fan (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Supervisor Nielson, Hanne Riis (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2007
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.
Series IMM-Thesis-2007-09
Keywords PEPA; Date Flow Analysis; Control Structure; Finite Automaton; Deadlock; Static Analysis; Stochastic Process Algebra
Fulltext
Original PDF imm5123.pdf (0.83 MB)
Admin Creation date: 2007-06-11    Update date: 2007-09-14    Source: dtu    ID: 200736    Original MXD