Analyzing the Control Structure of PEPA

Fan Yang, Hanne Riis Nielson

    Research output: Contribution to conferencePosterResearch


    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. We present a static analysis that very precisely approximates the control structure of processes expressed in PEPA. The analysis technique we adopted is Data Flow Analysis. 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. By annotating labels and layers to PEPA programs, the approximating result is very precise. Based on the analysis, we also develop algorithms for validating the deadlock property of PEPA programs. The techniques have been implemented in a tool which is able to analyze processes with a control structure that more than one thousand states.
    Original languageEnglish
    Publication date2007
    Publication statusPublished - 2007
    EventThe 14th International Static Analysis Symposium (SAS 2007) - Lyngby, Denmark
    Duration: 1 Jan 2007 → …


    ConferenceThe 14th International Static Analysis Symposium (SAS 2007)
    CityLyngby, Denmark
    Period01/01/2007 → …


    • PEPA, Date Flow Analysis, Control Structure, Finite Automaton, Deadlock, Static Analysis, Stochastic Process Algebra


    Dive into the research topics of 'Analyzing the Control Structure of PEPA'. Together they form a unique fingerprint.

    Cite this