Message from the General Chair

Program Committee Co-chairs Message (PDF)

pp. x-xi

Organizing Committee (PDF)

pp. xii

Technical Program Committee (PDF)

pp. xiii

Reviewers (PDF)

pp. xiv

Invited Talk

A Generic Mean Field Convergence Result for Systems of Interacting Objects (Abstract)

Jean-Yves Le Boudec, EPFL, I&C, Switzerland

David McDonald, University of Ottawa, Canada

Jochen Mundinger, EPFL, I&C, Switzerland

pp. 3-18

PDF

Session 1: Networking

A Petri Net Model for Evaluating Packet Buffering Strategies in a Network Processor (Abstract)

Girish B.C., Indian Institute of Science, India

R. Govindarajan, Indian Institute of Science, India

pp. 19-30

PDF

Session 2: Specification Formalisms

CSL^TA: an Expressive Logic for Continuous-Time Markov Chains (Abstract)

Susanna Donatelli, Universita di Torino, Italy

Serge Haddad, Universite Paris-Dauphine, France

Jeremy Sproston, Universita di Torino, Italy

pp. 31-40

PDF

Performance Trees: Expressiveness and Quantitative Semantics (Abstract)

Tamas Suto, Imperial College London, UK

Jeremy T. Bradley, Imperial College London, UK

William J. Knottenbelt, Imperial College London, UK

pp. 41-50

PDF

Cluster Grid based Response-time analysis module for the PIPE Tool (PDF)

Harini Kulatunga, Imperial College London, UK

Ashok Argent-Katwala, Imperial College London, UK

William Knottenbelt, Imperial College London, UK

pp. 51-52

The PEPA Plug-in Project (PDF)

Mirco Tribastone, The University of Edinburgh, UK

pp. 53-54

The ipclib PEPA Library (PDF)

Allan Clark, University of Edinburgh, UK

pp. 55-56

Session 3: Performance Analysis

Close form derivation of state-density functions over DBM domains in the analysis of non-Markovian models (Abstract)

L. Sassoli, Universita di Firenze, Italy

E. Vicario, Universita di Firenze, Italy

pp. 59-68

PDF

Relations in the Central Limit Theorem Version of the Response Time Law (Abstract)

Takayuki Osogami, IBM Tokyo Research Laboratory, Japan

pp. 69-78

PDF

Simultaneous Transient Analysis of QBD Markov Chains for all Initial Configurations using a Level Based Recursion (Abstract)

J. Van Velthoven, University of Antwerp, Belgium

B. Van Houdt, University of Antwerp, Belgium

C. Blondia, University of Antwerp, Belgium

pp. 79-90

PDF

Session 4: Automated Model Analysis

Interchange Formats for Performance Models: Experimentation and Ouput (Abstract)

Connie U. Smith, Performance Engineering Services, USA

Catalina M. Llado, Universitat de les Illes Balears, Spain

Ramon Puigjaner, Universitat de les Illes Balears, Spain

Lloyd G. Williams, PerX, USA

pp. 91-100

PDF

Automated Analysis of Simulation Traces - Separating Progress from Repetitive Behavior (Abstract)

Peter Kemper, College of William and Mary, USA

Carsten Tepper, Universitat Dortmund, Germany

pp. 101-110

PDF

Quantile Estimation for Performance Measures in Network Simulations with CINSim (PDF)

Daniel Ludtke, Technische Universitat Berlin, Germany

Dietmar Tutsch, Technische Universitat Berlin, Germany

Matthias Kuhm, Technische Universitat Berlin, Germany

pp. 111-112

Psi^2 a Software Tool for the Perfect Simulation of Finite Queueing Networks (PDF)

Jean-Marc Vincent, LIG Laboratory, Mescal Projet, France

Jerome Vienne, LIG Laboratory, Mescal Projet, France

pp. 113-114

GRIP: Generic Representatives in PRISM (PDF)

Alastair F. Donaldson, Codeplay Software Ltd., UK

Alice Miller, University of Glasgow, UK

David Parker, Oxford University, UK

pp. 115-116

Invited Talk

Session 5: Model Checking

Probabilistic Model-Checking Support for FMEA (Abstract)

Lars Grunske, University of Queensland, Australia

Robert Colvin, University of Queensland, Australia

Kirsten Winter, University of Queensland, Australia

pp. 119-128

PDF

Probabilistic Model Checking Modulo Theories (Abstract)

Bjorn Wachter, Saarland University, Germany

Lijun Zhang, Saarland University, Germany

Holger Hermanns, Saarland University, Germany

pp. 129-140

PDF

Session 6: Symbolic Analysis of Markov Chains

Signature-based Symbolic Algorithm for Optimal Markov Chain Lumping (Abstract)

Salem Derisavi, Carleton University, Canada

pp. 141-150

PDF

Dependability Analysis with Markov Chains: How Symmetries Improve Symbolic Computations (Abstract)

Michael G. McQuinn, University of Illinois at Urbana-Champaign, USA

Peter Kemper

William H. Sanders, University of Illinois at Urbana-Champaign, USA

pp. 151-160

PDF

Design of Experiments within the Mobius Modeling Environment (PDF)

Tod Courtney, University of Illinois at Urbana-Champaign, USA

Shravan Gaonkar, University of Illinois at Urbana-Champaign, USA

Michael G. McQuinn, University of Illinois at Urbana-Champaign, USA

Eric Rozier, University of Illinois at Urbana-Champaign, USA

William H. Sanders, University of Illinois at Urbana-Champaign, USA

Patrick Webster, University of Illinois at Urbana-Champaign, USA

pp. 161-162

PEPS2007 - Stochastic Automata Networks Software Tool (PDF)

Leonardo Brenner, LIG-ENSIMAG-ZIRST

Paulo Fernandes, PUCRS, Brazil

Brigitte Plateau, LIG-ENSIMAG-ZIRST

Ihab Sbeity, LIG-ENSIMAG-ZIRST

pp. 163-164

A framework to design and solve Markov Decision Well-formed Net models (PDF)

M. Beccuti, Univ. del Piemonte Orientale, Italy

D. Codetta-Raiteri, Univ. del Piemonte Orientale, Italy

G. Franceschinis, Univ. del Piemonte Orientale, Italy

Serge Haddad, Univ. de Paris Dauphine, France

pp. 165-166

Session 7: Process Algebra

Model checking the probabilistic pi-calculus (Abstract)

Gethin Norman, Oxford University, England

Catuscia Palamidessi, INRIA Futurs and LIX, Ecole Polytechnique, France

David Parker, Oxford University, England

Peng Wu, CNRS and LIX, Ecole Polytechnique, France

pp. 169-178

PDF

Symbolic Bisimulations for Probabilistic Systems (Abstract)

Peng Wu, CNRS and LIX, Ecole Polytechnqiue, France

Catuscia Palamidessi, INRIA Futurs and LIX, Ecole Polytechnique, France

Huimin Lin, Chinese Academy of Sciences, China

pp. 179-188

PDF

Basic Observables for Probabilistic May Testing (Abstract)

Maria Carla Palmeri, Universita di Firenze, Italy

Rocco De Nicola, Universita di Firenze, Italy

Mieke Massink, CNR-ISTI, Italy

pp. 189-200

PDF

Session 8: Performance Models

Performance Modeling of a Quorum Pattern in Layered Service Systems (Abstract)

Tariq Omari, Carleton University, Canada

Salem Derisavi, Carleton University, Canada

Greg Franks, Carleton University, Canada

Murray Woodside, Carleton University, Canada

pp. 201-210

PDF

CUT : Combining stochastic ordering and censoring to bound steady-state rewards and first passage time (PDF)

Jean-Michel Fourneau, INRIA project MESCAL, France; Universite Versailles St Quentin, France

Nihal Pekergin, Universite Paris 1, France; Universite Versailles St Quentin, France

Sana Younes, Universite Versailles St Quentin, France

pp. 211-212

Distritrack: Automated Average-Case Analysis (PDF)

David Hickey, National University of Ireland, Cork, Ireland

pp. 213-214

ProbDiVinE: A Parallel Qualitative LTL Model Checker (PDF)

Jiri Barnat, Masaryk University, Czech Republic

Lubos Brim, Masaryk University, Czech Republic

Ivana Cema, Masaryk University, Czech Republic

Milan Ceska, Masaryk University, Czech Republic

Jana Tumova, Masaryk University, Czech Republic

pp. 215-216

Invited Talk: A Process Algebra Master Equation (Abstract)

Luca Cardelli, Microsoft Research

pp. 219-226

PDF

Session 9: Stochastic Logic

Stochastic Game Logic (Abstract)

Christel Baier, Technische Universitat Dresden, Germany

Tomas Brazdil, Masaryk University, Czech Republic

Marcus Gr??er, Technische Universitat Dresden, Germany

Antonin Kucera, Masaryk University, Czech Republic

pp. 227-236

PDF

Qualitative Logics and Equivalences for Probabilistic Systems (Abstract)

Luca de Alfaro, University of California, Santa Cruz, USA

Krishnendu Chatterjee, University of California, Berkeley, USA

Marco Faella, Universita di Napoli "Federico II", Italy

Axel Legay, University of Liege, Belgium

pp. 237-248

PDF

Session 10: System Modelling

A business-oriented load dispatching framework for online auction sites (Abstract)

Daniel A. Menasce, George Mason University, USA

Vasudeva Akula, George Mason University, USA

pp. 249-258

PDF

Analysis of Local Address Scanning by Puppetnets (Abstract)

David M. Nicol, University of Illinois at Urbana-Champaign, USA

pp. 259-268

PDF

A Performance Analysis Tool for Scenario-Aware Streaming Applications (PDF)

B.D. Theelen, Eindhoven University of Technology, The Netherlands

pp. 269-270

PARTES: Performance Analysis of Real-Time Embedded Systems (PDF)

Benjamin Gorry, Heriot-Watt University, Scotland

Andrew Ireland, Heriot-Watt University, Scotland

Peter King, Heriot-Watt University, Scotland

pp. 271-272

A Productivity Centered Tools Framework for Application Performance Tuning (PDF)

H. Wen, IBM T.J. Watson Research Center, USA

S. Sbaraglia, IBM T.J. Watson Research Center, USA

S. Seelam, IBM T.J. Watson Research Center, USA

I. Chung, IBM T.J. Watson Research Center, USA

G. Cong, IBM T.J. Watson Research Center, USA

D. Klepacki, IBM T.J. Watson Research Center, USA

pp. 273-274

Session 11: Performance Analysis 2

Sample Path Analysis of Busy Periods and Related First Passages of a Correlated MEP/MEP/1 System (Abstract)

Chaitanya Garikiparthi, University of Missouri-Kansas City, USA

Appie van de Liefvoort, University of Missouri-Kansas City, USA

Kenneth Mitchell, University of Missouri-Kansas City, USA

pp. 277-286

PDF

Closed G-networks with Resets: product form solution (Abstract)

Jean-Michel Foumeau, Universite de Versailles Saint-Quentin, France; Projet MESCAL INRIA, France

pp. 287-296

PDF

Author Index

Author Index (PDF)

pp. 297