Multi-Workshop on Formal Methods in Performance Evaluation and Applications

Zaragoza, 6-10 of September 1999

Index page

Program of Tutorials and Workshops
Program of the Multiworkshop on: Petri Nets and Performance Models, Numerical Solutions of Markov Chains and Process Algebra and Performance Modelling

Monday 6
Tutorial Session: M.1
Validation and Evaluation: Properties and Bounds
09h00: Marta Kwiatkowska (University of Birmingham, U.K.)
Model checking of probabilistic systems against temporal logic specifications
10h30: Coffee break
11h00: Pierpaolo Degano, Corrado Priami (Univ. di Verona e Pisa, Italy)
Performance evaluation of mobile computations
12h30: --
13h00: Lunch
14h30: Mauro Pezzé (Politecnico di Milano, Italy)
Timed Petri nets
16h00: Coffee break
16h30: Javier Campos (Universidad de Zaragoza, Spain)
Properties and bounds on P/T nets
18h00: --
Tutorial Session:M.2
Solution and Analysis of Large Markov Chains
09h00: Tugrul Dayar (Bilkent University, Turkey)
Introduction to the numerical solution of Markov chains
10h30: Coffee break
11h00: Boudewjin Haverkort (University of Aachen, Germany)
Solution of infinite Markov chains
12h30: --
13h00: Lunch
14h30: Brigitte Plateau (Université de Grenoble, France)
Stochastic automata networks and Kronecker algebra
16h00: Coffee break
16h30: Gianfranco Ciardo (College of William and Mary, USA)
Efficient data structures and algorithms for the Kronecker approach
18h00: --
Workshop On Formal Methods And Manufacturing
08h45: Opening Session
09h00: R. Champagnat, R. Valette, H. Pingaud (LASS/LGC Toulouse, France)
Formal methods for batch production systems
10h00: G. Hetreux, C. Artigues, B. Palomino (ENSIGC Toulouse, LAIL Lille)
A two phase method for short term scheduling in batch processes
10h30: Coffee break
11h00: F. Balduzzi, A. Giua, C. Seatzu (Polit. Torino/ U. Cagliari, Italy)
Modelling automated manufacturing systems with hybrid automata
11h30: I. Demongodin, M. Mostefaoui, N. Sauer (Ecole des Mines de Nantes, France)
Liveness of hybrid marked graphs
12h00: L. Pietrac, B. Denis, J-J. Lesage (INSA-Lyon/ENS de Cachan, France)
An approach of formal meta-modeling for the design methods of automated manufacturing systems
12h30: --
13h00: Lunch
14h30: S. Kowaleski (U. of Dortmund, Germany)
Formal methods and the processing industries: status and prospects from an academic perspective
15h30: B.C Damasceno, X. Xie (Inria Metz, France)
Integration of scheduling and deadlock avoidance of manufacturing systems
16h00: Coffee break
16h30: E. Canuto, F. Balduzzi (Politecnico di Torino, Italy)
Manufacturing algebra: a formal method for modelling manufacturing systems
17h00: C. Haro, P. Martineau, C. Proust (E3I, Université de Tours, France)
A new generalized Petri net transformation
17h30: F. Basile, P. Chiacchio, V. Vittorini, Mazzocca (U. di Napoli I and II, Italy)
Modelling flexible manufacturing systems: a Petri net modular approach
18h00: --
Tuesday 7
Tutorial Session: T.1
Composition and Decomposition Methods
09h00: Ed Brinksma, Holger Hermanns (Univ. of Twente, The Netherlands)
Advances in Markovian and non Markovian process algebras
10h30: Coffee break
11h00: Claude Dutheillet (Université Paris 6, France)
Automatic exploitation of symmetries with SWNs
12h30: --
13h00: Lunch
14h30: Manuel Silva (Universidad de Zaragoza, Spain)
Net-driven decomposition techniques
16h00: --
Tutorial Session: T.2
Analysis of Non Markovian Petri Nets
09h00: Christoph Lindemann (University of Dortmund, Germany)
Deterministic stochastic Petri nets
10h30: Coffee break
11h00: Reinhard German (Technical University of Berlin, Germany)
Numerical analysis of non-Markovian stochastic Petri nets
12h30: --
13h00: Lunch
14h30: Susanna Donatelli (Univ. di Torino, Italy), Patrice Moreaux (Univ. de Reims, France)
Structured solution methods for GSPN with phase type distributions
16h00: --
Workshop On Formal Methods And Telecommunications
09h00: Opening Session (Chair: Marco Ajmone Marsan, Tomás Robles)
09h15: SDL (Chair: Tomás Robles)
  • J.Hintelmann (University of Essen, Germany)
    SDL based load and performance models for the design process of distributed systems
  • J.R. Vidal, L. Guijarro, V. Pla, J. Martínez (Univ. Politécnica de Valencia, Spain)
    An SDL modelling approach for performance evaluation of ATM networks
10h30: Coffee break
11h00: Case Studies (Chair: Marco Ajmone Marsan)
  • R. Khoussainov, A. Patel
    Formal modelling in embedded system design: a case study
  • S.Heymer, J.Grabowski (Medical University of Lubeck, Germany)
    Chemistry in action: discovering the behaviour of a network from local observations
  • M. Ionescu, A. Cavalli, (Institud National del Telecommunications, France)
    Embedded testing for the MAP-CSM protocol
12h30: --
13h00: Lunch
14h30: LOTOS (Chair: Tomás Robles)
  • G. Huecas, T. Robles (Univ. Politécnica de Madrid, Spain)
    L.F. Llana-Diaz, A. Verdejo (Universidad Complutense de Madrid, Spain)
    E-LOTOS: an overview
  • C. Shankland (University of Stirling, UK)
    A. Verdejo (U. Complutense de Madrid, Spain)
    Time, E-LOTOS, and the firewire
16h00: Coffee break
16h30: Petri Nets (Chair: Marco Ajmone Marsan)
  • B. Haverkort, A. Ost (Rheinish-Westfalishe Technische Hochschule, Aachen, Germany)
    Experiences in using infinite-state SPNs for modelling communication systems under self-similar traffic
  • M. Ajmone Marsan, R. Gaeta (Politecnico di Torino, Italy)
    GSPN and SWN models for ATM
17h45: --
Multiworkshop on:
Petri Nets and Performance Models,
Numerical Solutions of Markov Chains
Process Algebra and Performance Modelling
Wednesday 8
09h00: Opening Session
09h30: William H. Sanders (Invited-PNPM/University of Illinois, Champaign, U.S.A.):
Integrated frameworks for multi-level and multi-formalism modeling
10h30: Coffee break
Track: W.1
11h00: PN1: Techniques I (Chair: Marco Ajmone Marsan)
  • F. G. Vallés, J. M. Colom (Universidad de Zaragoza, Spain)
    Implicit places in net systems
  • E. Teruel (Univ. Zaragoza, Spain)
    G. Franceschinis (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
    M. De Pierro (Univ. Torino, Italy)
    Clarifying the priority specification of GSPN: detached priorities
  • D. Deavours, W. Sanders (University of Illinois, USA)
    An efficient well-specified check
12h30: --
13h00: Lunch
14h30: PN2: Applications to Telecommunication(Chair: Boudewijn Haverkort)
  • R. German, A. Heindl (TU Berlin, Germany)
    Performance evaluation of IEEE 802.11 wireless LANs with stochastic Petri nets
  • M. Meo, M. Ajmone Marsan (Politecnico di Torino, Italy)
    M. Sereno (Univ. di Torino, Italy)
    GSPN analysis of dual-band mobile telephony networks
15h30: Coffee Break
16h00: PN3: Non-Markovian Nets (Chair: Alessandro Giua)
  • R. German (TU Berlin, Germany)
    M. Telek (Tech. University of Budapest, Hungary)
    Formal relation of Markov renewal theory and supplementary variable in the analysis of stochastic Petri nets
  • M. Gribaudo, M. Sereno (Univ. di Torino, Italy)
    A. Bobbio (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
    Fluid stochastic Petri nets: an extended formalism to include non-Markovian models
  • A. Bobbio (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
    S. Garg (Lucent Techn., USA)
    M. Gribaudo, M. Sereno (Univ. di Torino, Italy)
    A. Horvarth, M. Telek (Tech. University of Budapest, Hungary)
    Modeling software systems with rejuvenation, restoration and checkpointing through fluid stochastic Petri nets
17h30: Tools session (Chair: Gianfranco Ciardo)
  • Peter Buchholz (TU Dresden)
    Peter Kemper (Unversitat Dortmund)
    Numerical analysis techniques in the APNN toolbox
  • Armin Zimmermann, Reinhard German, Jorn Freiheit, Gunter Hommel (TU Berlin)
    TimeNET 3.0 tool description
  • Gianfranco Ciardo, Andrew S. Miner (College of William and Mary)
    SMART - simulation and Markovian analyzer for reliability and timing
  • Graham Clark, Stephen Gilmore, Jane Hillston (University of Edinburgh)
    The PEPA performance modelling tools
  • Jean-Claude Hochon, Veronique Font (IXI, Toulouse)
    MISS-RdP interactive system modeling and simulation, performance evaluation by stochastic, colored and hybrid Petri nets
18h30: --
18h45: Reception
Track: W.2
11h00: MC1: Infinite Markov Chains (Chair: William J. Stewart)
  • R. Sadre, Boudewijn Haverkort, A. Ost (Rheinish-Westfalishe Technische Hochschule, Aachen, Germany)
    An efficient and accurate decomposition method for open finite and infinite buffer queueing networks
  • G. Ciardo, A. Riska, E. Smirni (College of William and Mary, Williamsburg, USA)
    An aggregation-based solution method for M/G/1-type processes
  • I. Adan, J. Resing (Eidhoven University of Technology, The Netherlands)
    A class of Markov processes on a semi-infinite strip
12h30: --
13h00: Lunch
14h30: PA1: Non-Markovian SPA (Chair: Jane Hillston)
  • A. El-Rayes, M. Kwiatkowska, G. Norman (University of Birmingham, UK)
    Solving infinite stochastic process algebra models through matrix-geometric methods
  • G. Clark (University of Edinburgh, UK)
    Stochastic process algebra structure for insensitivity
15h30: Coffee Break
16h00: MC2: Distributed and Parallel Solutions (Chair: Brigitte Plateau)
  • W. Knottenbelt, P. Harrison (Imperial College, London, UK)
    Distributed disk-based solution techniques for large Markov models
  • P. Buchholz, M. Fischer, P. Kemper (Universitat Dortmund, Germany)
    Distributed steady state analysis using Kronecker algebra
  • V. Migallon, J. Penades (Universidad de Alicante, Spain)
    D. Szyld (Temple University, Philadelphia, USA)
    Experimental study of parallel iterative solution of Markov chains with block partitions
17h30: MCP: Poster Session (Chair: Brigitte Plateau)
  • J.M. Fourneau (Université de Versailles Saint Quentin, France)
    Stochastic automata networks: using structural properties to reduce the state space
  • M. Jarraya, D. El Baz (LAAS, Toulouse, France)
    Asynchronous iterations for the solution of Markov systems
  • F. Quessette, A. Troubnikoff (Université de Versailles Saint Quentin, France)
    Using of non-symmetric permutations to solve large Markov models
  • D. Twigg, A. Ramesh, U. Sandadi, A. Anand, C. Sharma (The Boeing Company, USA)
    Reliability computation of systems that operate multiple phases and multiple missions
18h30: --
18h45: Reception
Thursday 9
09h00: Marcel Neuts (Invited-NSMC/University of Arizona, U.S.A.)
Some recent new problems and results in matrix-analytic methods
Track: T.1
10h00: PN4 (Chair: Alois Ferscha)
  • W. Zuberek (Memorial University of Nfld, Canada)
    Stepwise refinements of net models and their place invariants
10h30: Coffee break
11h00: PN5: Techniques II (Chair: Peter Kemper)
  • B. Haverkort, H. Bohnenkamp, A. Bell (RWTH Aachen, Germany)
    On the efficient sequential and distributed evaluation of very large stochastic Petri nets
  • G. Ciardo, A. Miner (College of William and Mary, USA)
    A data structure for the efficient Kronecker solution of GSPNs
  • C. J. Pérez-Jiménez, J. Campos (Universidad de Zaragoza, Spain)
    On state space decomposition for the numerical analysis of stochastic Petri nets
12h30: --
13h00: Lunch
14h30: PN6: Formalisms (Chair: Javier Campos)
  • P. Kemper (Universitaet Dortmund, Germany)
    A mapping of autonomous net condition event systems to GSPNs
  • R. Gaeta (Univ. di Torino, Italy)
    A. Bobbio, G. Franceschinis, L. Portinale (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
    Exploiting Petri nets to support fault tree based dependability analysis
15h30: Coffee Break
16h00: Max/Plus (Organiser: E. Wagneur)
  • S. Gaubert (INRIA, Domaine de Volueau, France)
    J. Mairesse (CNRS- Université, France)
    Performance evaluation of timed Petri nets using heaps of pieces
  • S. Lahaye, J. L. Boimond, L. Hardouin (LISA, Univ. Angers, France)
    Optimal control of (min, +) linear time-varying systems
  • I. Demongodin, E. Wagneur (IRCYN, CNRS, E. Mines de Nantes, France)
    On the rational use of Petri nets, automata and the max-plus algebra for the optimal control of DEDS
17h30: --
Track: T.2
10h00: MC3: Modelling techniques
  • R. German (Teschnische Universitat Berlin, Germany)
    Cascaded deterministic and stochastic Petri nets
10h30: Coffee break
11h00: MC4: Computational and storage Issues (Chair: Tugrul Dayar)
  • I. Sonin, J. Thornton (UNC Charlotte, USA)
    Computational properties of algorithm "REFUND" for the fundamental/group inverse matrix of a Markov chain
  • P. Buchholz (Universitat Dortmund, Germany)
    Projection methods for the analysis of stochastic automata networks
  • S. Racz, M. Telek (Technical University of Budapest, Hungary)
    Performability analysis of Markov reward models with rate and impulse reward
  • H. Hermanns (University of Twente, The Netherlands)
    J. Kayser, M. Siegle (University of Erlangen-Nurnberg, Germany)
    Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains
12h30: --
13h00: Lunch
14h30: MC5: Bounds (Chair: Jean-Michel Fourneau)
  • S. Donatelli (Univ. de Torino, Italy)
    S. Haddad (Université de Paris-Dauphine, France)
    P. Moreaux, M. Sene (Université de Reims, France)
    Bounds for rewards of systems with client/server interaction
  • T. Dayar (Bilkent University, Ankara, Turkey)
    N. Pekergin (Université de Versailles Saint Quentin, France)
    Stochastic comparison, reorderings and NCD Markov chains
15h30: Coffee Break
16h00: PA2: Interactions in SPA models (Chair: Ulrich Herzog)
  • J. Bradley, N. Davies (University of Bristol, UK)
    Reliable performance modelling with approximate synchronisations
  • M. Bravetti, R. Gorrieri (University of Bologna, Italy)
    Interactive generalized semi-Markov processes
  • H. Bohnenkamp, B. Haverkort (Rheinish-Westfalishe Technische Hochschule, Aachen, Germany)
    Stochastic event structures for the decomposition of stochastic process algebra models
17h30: --
Friday 10
09h00: R. Gorrieri (Invited-PAPM/University of Bologna, Italy)
Stochastic Process algebras: past and future
Track: F.1
10h00: PN7 (Chair: Falko Bause)
  • V. Valero Ruiz, F. Cuartero Gómez (Universidad de Castilla-La Mancha, Spain)
    D. de Frutos Escrig (Univ. Complutense, Spain)
    On non-decidability of reachability of timed-arc Petri nets
10h30: Coffee break
11h00: PN8: Timed Nets (Chair: Guy Juanole)
  • M. Boyer, M. Diaz (LAAS/CNRS, France)
    Non equivalence between Time Petri Nets and Time Stream Petri Nets
  • B. Pradin-Chezalviel, R. Valette (LAAS-CNRS, France)
    L.A. Kunzle (CEFET-PR, Brasil)
    Scenario durations charaterization of t-timed Petri nets using linear logic
  • X. Li, J. Lilius (Turku Centre for Computer Science, Finland)
    Checking time Petri nets for linear duration properties
12h30: --
13h00: Lunch
14h30: MC7: Phase Type Systems (Chair: Gianfranco Ciardo)
  • D. Bini, B. Meini (Univ. de Pisa, Italy)
    S. Chakravarthy (Kettering University, Flint, USA)
    A new algorithm for the design of finite capacity service units
  • U. Krieger (Deutsche Telekom, Darmstadt, Germany)
    V. Naumov (Lappeenranta University of Technology, Finland)
    Analysis of a delay-loss system with a superimposed Markovian arrival process and state-dependent service times
15h30: Closing Session
16h00: --
Track: F.2
10h00: PA3: Probabilistic I/O Automata (Chair: Roberto Gorrieri)
  • E.W. Stark, G. Pemmansani (State University of New York, Stony Brook, USA)
    Implementation of a compositional performance analysis algorithm for probabilistic I/O automata
10h30: Coffee break
11h00: MC6: Applications (Chair: Udo Krieger)
  • A. Demir, P. Feldmann (Bell laboratories, Murray Hill, USA)
    Modelling and simulation of interference noise in electronic integrated circuits using Markov chain models
  • M-A. Remiche (Université Libre de Bruxelles, Belgium)
    Efficiency of an IPhP^3 illustrated through a model in cellular networks
  • John Lui, W. Lam (The Chinese University of Hong Kong, Shatin, NT)
    A general methodology in analyzing the performance ofparallel/distributed simulation under general computational graphs
12h30: --
13h00: Lunch
14h30: PA4: SPA Case Studies (Chair: Marina Ribaudo)
  • L. Kloul, J.M. Fourneau, F. Valois (Université de Versailles-Saint Quentin, France)
    Performance modelling of hierarchical cellular networks using PEPA
  • A. Aldini, M. Bernardo, R. Gorrieri (University of Bologna, Italy)
    An algebraic model for evaluating the performance of an ATM switch with explicit rate marking
15h30: Closing Session
16h00: --
Last modified: June 15, 1999