Conference Program

Proccedings of the Petri Net 2009 conference will be published in Springer's LNCS (volume 5606)

Program details

22 juin 2009

8h00
9h00
10h00
11h00
12h00
13h00
14h00
15h00
16h00
17h00
18h00
Break
Lunch
Break
APNOC
Keynote

Session 1

Session 2

Session 3

PNSE
Opening + Keynote 1

Session 1

Session 2

Session 3

TUT0
Basic Net Classes(1)

Basic Net Classes(2)

Coloured Petri Nets(1)

Coloured Petri Nets(2)

TUT1
Biomodel Engineering(1)

Biomodel Engineering(2)

Biomodel Engineering(3)

Biomodel Engineering(4)

[APNOC] Keynote

  • From 09h30 to 10h30, herpin
  • Chair:
  • Paper list:
    • Abstraction And Approximation in Abstract Interpretation
      • By: Radhia Cousot

[APNOC] Session 1

  • From 11h00 to 12h30, herpin
  • Chair:
  • Paper list:
    • Opacity And Abstractions
      • By: Jérémy Dubreil
    • Workflow Soundness And Data Abstraction
      • By: Nikola Trcka

[APNOC] Session 2

  • From 14h00 to 15h30, herpin
  • Chair:
  • Paper list:
    • Abstraction Techniques For Performance Analysis by Simulation
      • By: Helen Schonenberg
    • Abstracting Common Business Rules to Petri Nets
      • By: Kees Van Hee, Jan Hidders, Geert-Jan Houben, Jan Paredaens And Phillipe Thiran

[APNOC] Session 3

  • From 16h00 to 17h30, herpin
  • Chair:
  • Paper list:
    • Vicinity Respecting Homomorphisms For Abstracting System Requirements
      • By: Jörg Desel And Agathe Merceron
    • Reachabilty Analysis For Recursive Petri Nets With Shared Places
      • By: Djaouida Dahmani, Jean Michel Ilié And Malika Boukala

[PNSE] Opening + Keynote 1

  • From 09h15 to 10h30, durand
  • Chair:
  • Paper list:
    • Opening
      • By: Daniel Moldt
    • Petri Nets to Define The Control Structure of Systems
      • By: Christophe Sibertin-Blanc

[PNSE] Session 1

  • From 11h00 to 12h25, durand
  • Chair:
  • Paper list:
    • Net Components: Concepts, Tool, Praxis
      • By: Lawrence Cabac
    • Modeling With Net References And Synchronous Channels Submission
      • By: Heiko Rölke
    • On The Multilevel Petri Nets-Based Models in Project Engineering
      • By: Sarka Kvetonova And Vladimir Janousek

[PNSE] Session 2

  • From 14h00 to 15h25, durand
  • Chair:
  • Paper list:
    • Let's Play The Token Game-Model Transformations Powered by Colored Petri Nets
      • By: Manuel Wimmer, Angelika Kusel, Johannes Schoenboeck, Thomas Reiter, Werner Retschitzegger And Wielan
    • On The Dynamic Features of Pntalk
      • By: Radek Koci And Vladimir Janousek
    • United-a Petri Net Based Modeling Framework For Complex, Adaptive Systems
      • By: Marcin Hewelt And Matthias Wester-Ebbinghaus

[PNSE] Session 3

  • From 16h00 to 17h35, durand
  • Chair:
  • Paper list:
    • Composition of Concerns Using Reference Nets
      • By: Joao Paulo Barros, Isabel Sofia Brito And Elisabete Soeiro
    • Modeling And Prototyping of Concurrent Software Architectural Designs With Colored Petri Nets
      • By: Robert Pettit Iv, Hassan Gomaa And Julie Fant
    • A Colored Petri Nets Model For The Diagnosis of Semantic Faults of Bpel Services
      • By: Yingmin Li, Tarek Melliti And Philippe Dague

[TUT0] Basic Net Classes(1)

  • From 09h00 to 10h30, 211/55-65
  • Chair: Wolfgang Reisig And Joerg Desel
  • Paper list:
    • History, Philosophy, And Principles of Net Theory
      • By: Wolfgang Reisig
    • Introduction to P/T-Systems: Examples And Definitions, Behavioural Properties
      • By: Joerg Desel

[TUT0] Basic Net Classes(2)

  • From 11h00 to 12h30, 211/55-65
  • Chair: Joerg Desel, Jetty Kleijn
  • Paper list:
    • Elementary Nets-Systems: Intuition, Examples And Definitions, Fundamental Situations, Sequential And Non-Sequential Behaviour of En-Systems
      • By: Jetty Kleijn
    • Basic Analysis Techniques : Linear Algebra Techniques(Invariants) And Structural Techniques; Restricted Net Classes; Causal Semantics of P/T-Systems
      • By: Joerg Desel

[TUT0] Coloured Petri Nets(1)

  • From 14h00 to 15h30, 211/55-65
  • Chair: Kurt Jensen
  • The CPN modelling language including hierarchical nets and timed nets

[TUT0] Coloured Petri Nets(2)

  • From 16h00 to 17h30, 211/55-65
  • Chair: Kurt Jensen
  • State spaces, behavioural properties and examples of industrial applications

[TUT1] Biomodel Engineering(1)

  • From 09h00 to 10h30, 207/56-66
  • Chair: Monika Heiner, Rainer Breitling, David Gilbert
  • Introduction: Systems biology, synthetic biology
    Conceptual modelling framework
    BioModel Engineering
    From cell biology to Petri nets

    More information, materials, etc: http://www-dssz.informatik.tu-cottbus.de/BME

[TUT1] Biomodel Engineering(2)

  • From 11h00 to 12h30, 207/56-66
  • Chair: Monika Heiner, Rainer Breitling, David Gilbert
  • From cell biology to Petri nets (2)
    Static Petri net analysis (qualitative)

    More information, materials, etc: http://www-dssz.informatik.tu-cottbus.de/BME

[TUT1] Biomodel Engineering(3)

  • From 14h00 to 15h30, 207/56-66
  • Chair: Monika Heiner, Rainer Breitling, David Gilbert
  • Conceptual modelling framework & paradigms in detail: (QPN), SPN, CPN
    Model checking (1): Analytical vs simulative model checking, model checking in the 3 worlds

    More information, materials, etc: http://www-dssz.informatik.tu-cottbus.de/BME

[TUT1] Biomodel Engineering(4)

  • From 16h00 to 17h30, 207/56-66
  • Chair: Monika Heiner, Rainer Breitling, David Gilbert
  • Model checking (2): Model checking for BME: parameter fitting, database searching, model comparison
    Open problems & challenges for PN community
    What we have not covered

    More information, materials, etc: http://www-dssz.informatik.tu-cottbus.de/BME

23 juin 2009

8h00
9h00
10h00
11h00
12h00
13h00
14h00
15h00
16h00
17h00
18h00
Break
Lunch
Break
ORGMOD
Opening + Session 1

Session 2

From Agr to Masq:...

Poster Session

Session 3

PNSE
Session 4

Session 5

From Agr to Masq:...

Poster Session

Session 6 + Closing

TISTO
Computing...

Session 1

Using a Stochastic...

Session 2

Session 3

TUT0
Timed & Stochastic Nets(1)

Timed & Stochastic Nets(2)

TUT5
Computer-Aided Formal...(1)

Computer-Aided Formal...(2)

TUT2
Evaluating Concurrent...(1)

Evaluating Concurrent...(2)

TUT3
Continuous Petri Nets:...(1)

Continuous Petri Nets:...(2)

TUT4
The Petri Net Markup...(1)

The Petri Net Markup...(2)

TUT6
System-Level Modeling...(1)

System-Level Modeling...(2)

[ORGMOD] Opening + Session 1

  • From 09h45 to 10h30, astier
  • Chair:
  • Paper list:
    • Support For Modeling Roles And Dependencies in Multi-Agent Systems
      • By: Lawrence Cabac And Daniel Moldt

[ORGMOD] Session 2

  • From 11h00 to 12h30, astier
  • Chair:
  • Paper list:
    • an Approach For Building Holonic Models of Design Processes For Knowledge Management
      • By: Achraf Ben Miled, Vincent Hilaire, Davy Monticolo And Abderrafiaa Koukam
    • Reorganisation And Self-Organisation in Multi-Agent Systems
      • By: Gauthier Picard, Jomi Hübner And Boissier Olivier
    • a Tool For Creation And Deployment of Organization Models
      • By: Endri Deliu

[ORGMOD] From Agr to Masq: Understanding Organizations From a Multi-Agent Point of View

  • From 14h00 to 15h00, durand
  • Speaker: Jacques Ferber
  • Paper list:

[ORGMOD] Session 3

  • From 16h00 to 17h30, astier
  • Chair:
  • Paper list:
    • Last Posters
      • By:
    • Modeling an Open And Controlled System Unit as a Modular Component of Systems of Systems
      • By: Matthias Wester-Ebbinghaus And Daniel Moldt
    • Multi Agent Organisation For Coevolutionary Optimization
      • By: Grégoire Danoy, Pascal Bouvry And Boissier Olivier
    • Closing
      • By: Daniel Moldt

[PNSE] Session 4

  • From 09h00 to 10h30, durand
  • Chair:
  • Paper list:
    • Schedule-Aware Workflow Management Systems
      • By: Ronny Mans, Nick Russell, Wil Van Der Aalst, Arnold Moleman And Piet Bakker
    • Synthesis of Ptl-Nets With Partially Localised Conflicts
      • By: Maciej Koutny And Marta Pietkiewicz-Koutny
    • Verics 2008-a Model Checker For Time Petri Nets And High-Level Languages
      • By: Verics Group

[PNSE] Session 5

  • From 11h00 to 12h25, durand
  • Chair:
  • Paper list:
    • Bounded Parametric Model Checking For Elementary Net Systems
      • By: Michał Knapik, Wojciech Penczek And Maciej Szreter
    • Managing Complexity in Model Checking With Decision Diagrams For Algebraic Petri Net
      • By: Didier Buchs And Steve Hostettler
    • Model Analysis Via a Translation Schema to Coloured Petri Nets
      • By: Visar Januzaj And Stefan Kugele

[PNSE] From Agr to Masq: Understanding Organizations From a Multi-Agent Point of View

  • From 14h00 to 15h00, durand
  • Speaker: Jacques Ferber
  • Paper list:

[PNSE] Session 6 + Closing

  • From 16h00 to 17h30, durand
  • Chair: Michael Köhler And Olivier Bossier
  • Paper list:
    • Last Posters
      • By:
    • Sat-Based(Parametric) Reachability For Time Petri Nets
      • By: Wojciech Penczek, Agata Półrola And Andrzej Zbrzezny
    • Transforming Ws-Cdl Specifications Into Coloured Petri Nets
      • By: Valentin Valero, Hermenegilda Macia And Enrique Martinez
    • Closing
      • By: Daniel Moldt

[TISTO] Computing Probabilities Over Dbm Domains to Integrate Qualitative Verification And Quantitative Evaluation of Timed Stochastic Models

  • From 09h00 to 10h30, herpin
  • Chair: Enrico Vicario
  • Paper list:
    • Computing Probabilities Over Dbm Domains to Integrate Qualitative Verification And Quantitative Evaluation of Timed Stochastic Models
      • By: Enrico Vicario

[TISTO] Session 1

  • From 11h00 to 12h30, herpin
  • Chair:
  • Paper list:
    •  petri Nets With Time Windows: Possibilities And Limitations
      • By: Jan-Thierry Wegener, Benjamin Collins And Louchka Popova-Zeugmann
    • Unfolding of Time Petri Nets For Quantitative Time Analysis
      • By: Sogbohossou Medesu And David Delfieu
    • A Two Step Algorithm to Improve Systems Optimization Based on The State Space Exploration For Timed Coloured Petri Net Models
      • By: Miguel Antonio Mujica And Miquel Angel Piera

[TISTO] Using a Stochastic π-Calculus For Temporal Parameters Inference in Gene Regulatory Networks

  • From 14h00 to 15h00, herpin
  • Chair: Morgan Magnin, Loic Pauleve And Olivier f. Roux
  • Paper list:
    • Using The Stochastic Pi-Calculus For Temporal Parameters Inference in Gene Regulatory Networks
      • By: Loic Pauleve, Olivier f. Roux

[TISTO] Session 2

  • From 15h00 to 15h30, herpin
  • Chair:
  • Paper list:
    • Hybrid Adaptive Petri Nets For Modeling And Analyzing Biochemical Systems
      • By: Hongkun Yang And Huan Zhou

[TISTO] Session 3

  • From 16h00 to 16h30, herpin
  • Chair:
  • Paper list:
    • Organizational Patterns Are Effective For Large Scale Organizations
      • By: Satoshi Hattori

[TUT5] Computer-Aided Formal Verification And Validation(1)

  • From 09h00 to 10h30, 245-atrium
  • Chair: Bret Michael
  • The aim of this tutorial is to introduce the attendee to the basics of computer-aided formal verification and validation (V&V). The tutorial begins with the motivation for conducting computer-aided formal V&V and an introduction to what is known as the System Reference Model Framework for conducting formal V&V, distinguishing formal V&V and the framework from the traditional view of V&V of systems. The SRM Framework relies on assertion-based specifications.

    The tutorial lays out the process for systematically developing these specifications, in support of both formal validation and executable model checking (i.e., combining runtime verification with automatic test generation). The context of the first part of the tutorial will be given from the perspective of conducting independent V&V (IV&V). The second part of the tutorial covers the basics of writing formal assertions and using assertion statecharts. The tutorial concludes with coverage of some advanced topics such as the use of validation scenario patterns and nondeterministic statecharts.

[TUT5] Computer-Aided Formal Verification And Validation(2)

  • From 11h00 to 12h30, 245-atrium
  • Chair: Bret Michael
  • The aim of this tutorial is to introduce the attendee to the basics of computer-aided formal verification and validation (V&V). The tutorial begins with the motivation for conducting computer-aided formal V&V and an introduction to what is known as the System Reference Model Framework for conducting formal V&V, distinguishing formal V&V and the framework from the traditional view of V&V of systems. The SRM Framework relies on assertion-based specifications.

    The tutorial lays out the process for systematically developing these specifications, in support of both formal validation and executable model checking (i.e., combining runtime verification with automatic test generation). The context of the first part of the tutorial will be given from the perspective of conducting independent V&V (IV&V). The second part of the tutorial covers the basics of writing formal assertions and using assertion statecharts. The tutorial concludes with coverage of some advanced topics such as the use of validation scenario patterns and nondeterministic statecharts.

[TUT2] Evaluating Concurrent Software Architectures Using Petri Nets(1)

  • From 09h00 to 10h30, 249-atrium
  • Chair: Rob Pettit
  • The domain of real-time, concurrent, and embedded software is becoming increasing complex. To effectively develop and deploy these systems, greater care must be taken to construct adequate models of the software and to effectively analyze and evaluate software design decisions prior to code development. In this tutorial, we will discuss the software architecture design modeling of software systems in terms of concurrent task behavior. We will then explore the application of Petri nets (specifically Colored Petri Nets) in evaluating a concurrent software architecture design and assessing its behavioral characteristics prior to software implementation. In this way, we can more effectively argue about the validity of the software behavior in the early lifecycle stages when correcting a problem is much less costly.   

    The software design modeling will nominally be based on the Unified Modeling Language (UML), but we will also discuss how other approaches such as AADL or structured analysis and design can be evaluated with this approach. The Petri net evaluation will be conducted using CPNTools.

    A case study will be used throughout the tutorial to illustrate the modeling and evaluation methods. The case study will also be constructed incrementally to illustrate how the fidelity of the analytical results increases with the maturity of the design model.

[TUT2] Evaluating Concurrent Software Architectures Using Petri Nets(2)

  • From 11h00 to 12h30, 249-atrium
  • Chair: Rob Pettit
  • The domain of real-time, concurrent, and embedded software is becoming increasing complex. To effectively develop and deploy these systems, greater care must be taken to construct adequate models of the software and to effectively analyze and evaluate software design decisions prior to code development. In this tutorial, we will discuss the software architecture design modeling of software systems in terms of concurrent task behavior. We will then explore the application of Petri nets (specifically Colored Petri Nets) in evaluating a concurrent software architecture design and assessing its behavioral characteristics prior to software implementation. In this way, we can more effectively argue about the validity of the software behavior in the early lifecycle stages when correcting a problem is much less costly.   

    The software design modeling will nominally be based on the Unified Modeling Language (UML), but we will also discuss how other approaches such as AADL or structured analysis and design can be evaluated with this approach. The Petri net evaluation will be conducted using CPNTools.

    A case study will be used throughout the tutorial to illustrate the modeling and evaluation methods. The case study will also be constructed incrementally to illustrate how the fidelity of the analytical results increases with the maturity of the design model.

[TUT3] Continuous Petri Nets: Expressivity, Analysis And Control of a Class of Hybrid Systems(1)

  • From 14h00 to 15h30, 211/55-65
  • Chair: Manuel Silva
  • Special tutorial in memory of Prof. Laura Recalde

    - From 14h00 to 14h45 / Manuel Silva: Fluidification and basic properties of continuous Petri net models.
    - From 14h45 to 15h30 / Serge Haddad: On the computational power of Timed Differentiable Petri nets.

    More detail is available at http://petrinets2009.lip6.fr/recalde.html

[TUT3] Continuous Petri Nets: Expressivity, Analysis And Control of a Class of Hybrid Systems(2)

  • From 16h00 to 17h30, 211/55-65
  • Chair: Manuel Silva
  • Special tutorial in memory of Prof. Laura Recalde

    - From 16h00 to 16h45 / Manuel Silva: Observability, Steady-state analysis and parametric optimisation of Continuous PNs under infinite servers’ semantics.
    - From 16h45 to 17h30 / Alessandro Giua: Fault diagnosis and Control of Continuous PNs under infinite servers’ semantics.

    More detail is available at http://petrinets2009.lip6.fr/recalde.html

[TUT4] The Petri Net Markup Language, Theory And Practice(1)

  • From 14h00 to 15h30, 245-atrium
  • Chair: Lom Hillah, Ekkart Kindler
  • During this session, the theoretical concepts of PNML will be presented, along with their corresponding XML syntax. The focus will be on these concepts as formulated in terms of meta-models. We will show why we have adopted this approach, the expected benefits and how the design process was articulated.

    Detailed information is available at http://www.pnml.org/tutorialpn09.php

[TUT4] The Petri Net Markup Language, Theory And Practice(2)

  • From 16h00 to 17h30, 245-atrium
  • Chair: Lom Hillah, Ekkart Kindler
  • This session will cover the implementation of PNML. We will show how an existing tool can be extended for supporting PNML on the basis of the PNML Framework, which is a reference implementation of the standard. The purpose of the framework is to help tools developers in making their tools PNML conformant. If attendants are interested, a practical and easy to complete hands-on tutorial will take place.

    Detailed information is available at http://www.pnml.org/tutorialpn09.php

[TUT6] System-Level Modeling And Validation of Continuous/Discrete Systems(1)

  • From 14h00 to 15h30, 249-atrium
  • Chair: Gabriela Nicolescu
  • The 2007 edition of ITRS (The International Technology Roadmap for Semiconductors) emphasizes the "More Than Moore's Law" trend. This trend focuses on system integration rather than transistor density and will lead to a functional diversification in integrated systems. This diversification allows for non-digital functionalities such as RF, power control, optical and/or mechanical components, sensors and actuators to migrate from the system-board level into a package-level SiP) or chip-level (SoC) implementation. These systems enable new application and open new markets. They will be found in key domains like transport, security, health, energy. The system-level modeling and validation of these systems is still a challenge, one of the main issues being the interfacing of continuous and discrete components. Currently, the design of the continuous/discrete interfaces represents a time consuming and error-prone stage in the design flow.

    This tutorial introduces a generic methodology for the design of tools enabling the global modeling and validation for continuous/discrete heterogeneous systems. Before the implementation stage, the methodology proposes several steps enabling the gradual formal definition and verification of the continuous/discrete interfaces.

    G. Nicolescu is Associate Professor at Ecole Polytechnique de Montréal in Canada, Department of Computer and Software Engineering. She holds a Ph.D. degree from National Polytechnic Institute of Grenoble, France (Prize for the best Microelectronics dissertation). Before joining Ecole Polytechnique de Montreal, Dr Nicolescu has completed a postdoctoral (NSERC-NATO industrial scholarship) at STMicoelectronics Central R&D Ottawa. Her current research interests are related with system-level design, modelling and simulation methodologies for heterogeneous systems-on-chip.

[TUT6] System-Level Modeling And Validation of Continuous/Discrete Systems(2)

  • From 16h00 to 17h30
  • Chair: Gabriela Nicolescu
  • The 2007 edition of ITRS (The International Technology Roadmap for Semiconductors) emphasizes the "More Than Moore's Law" trend. This trend focuses on system integration rather than transistor density and will lead to a functional diversification in integrated systems. This diversification allows for non-digital functionalities such as RF, power control, optical and/or mechanical components, sensors and actuators to migrate from the system-board level into a package-level SiP) or chip-level (SoC) implementation. These systems enable new application and open new markets. They will be found in key domains like transport, security, health, energy. The system-level modeling and validation of these systems is still a challenge, one of the main issues being the interfacing of continuous and discrete components. Currently, the design of the continuous/discrete interfaces represents a time consuming and error-prone stage in the design flow.

    This tutorial introduces a generic methodology for the design of tools enabling the global modeling and validation for continuous/discrete heterogeneous systems. Before the implementation stage, the methodology proposes several steps enabling the gradual formal definition and verification of the continuous/discrete interfaces.

    G. Nicolescu is Associate Professor at Ecole Polytechnique de Montréal in Canada, Department of Computer and Software Engineering. She holds a Ph.D. degree from National Polytechnic Institute of Grenoble, France (Prize for the best Microelectronics dissertation). Before joining Ecole Polytechnique de Montreal, Dr Nicolescu has completed a postdoctoral (NSERC-NATO industrial scholarship) at STMicoelectronics Central R&D Ottawa. Her current research interests are related with system-level design, modelling and simulation methodologies for heterogeneous systems-on-chip.

24 juin 2009

8h00
9h00
10h00
11h00
12h00
13h00
14h00
15h00
16h00
17h00
18h00
Register
Opening Session
Keynote
Joseph Sifakis

Break
Lunch
Keynote
Bernard Courtois

Break
PN
Session 1

Session 2

Tools Demonstration

RSP
Session 1: Formal...

Session 2:...

From 19h00 to 20h30: Reception at The Hôtel de Ville de Paris.

Component-Based Construction of Heterogeneous Real-Time Systems in Bip

  • From 09h00 to 10h00, durand
  • Speaker: Joseph Sifakis
  • We present a framework for the component-based construction of real-time systems. The framework is based on the BIP (Behaviour, Interaction, Priority)semantic model, characterized by a layered representation of components. Compound components are obtained as the composition of atomic components specified by their behaviour and interface, by using connectors and dynamic priorities. Connectors describe structured interactions between atomic components, in terms of two basic protocols: rendezvous and broadcast. Dynamic priorities are used to select amongst possible interactions - in particular, to express scheduling policies.

    The BIP framework has been implemented in a language and a toolset. The BIP language offers primitives and constructs for modelling and composing atomic components described as state machines, extended with data and functions in C. The BIP toolset includes an editor and a compiler for generating from BIP programs, C++ code executable on a dedicated platform. It also allows simulation and verification of BIP programs by using model checking techniques.

    BIP supports a model-based design methodology involving three steps:

    1) The construction of a system model from a set of atomic components composed by progressively adding interactions and priorities;

    2) The application of incremental verification techniques. These techniques use the fact that the designed system model can be obtained by successive application of property-preserving transformations in a three-dimensional space: Behavior×Interaction×Priority.

    3) The generation of correct-by-construction distributed implementations from the designed model. This is achieved by source-to-source transformations which preserve global state semantics.

    We provide two examples illustrating the methodology.

    Further information is available at: http://www-verimag.imag.fr/~async/bip.php

Prototyping Custom Circuits And Systems: 20 Years Back, x Years Forward

  • From 14h00 to 15h00, durand
  • Speaker: Bernard Courtois
  • Infrastructures to provide access to custom integrated hardware manufacturing facilities are important because they allow Students and Researchers to access professional facilities at a reasonable cost, for their prototyping needs. Such facilities are otherwise difficult to obtain directly from manufacturers. In the late 70s/early 80s, pioneering integrated circuits Multi-Chip Projects / Multi-Project Wafers initiatives have been launched in Europe, Asia, and North America. Some of these initiatives work together and today a worldwide cooperation has been established by the most experienced. The talk will first review these initiatives and the motivations for a global cooperation scheme. These initiatives helped the development of EE&CS communities. The talk next advocates that other communities like the BioMed community could also take advantage of them. Examples of BioMed applications using CMOS and MEMS are given. Important applications like energy management are also addressed. The talk will conclude on where manufacturing infrastructures like CMP should go, considering technical developments towards More Moore, More than Moore, as well as statements related to globalization.

[PN] Session 1

  • From 10h30 to 12h10, durand
  • Chair: Maciej Koutny
  • Paper list:
    • The Universal Net Composition Operator
      • By: Wolfgang Reisig
    • Towards a Standard For Modular Petri Nets: a Formalisation
      • By: Ekkart Kindler, Laure Petrucci
    • Asap: an Extensible Platform For State Space Analysis
      • By: Michael Westergaard, Sami Evangelista, Lars m. Kristensen
    • The Access/Cpn Framework: a Tool For Interacting With The Cpn Tools Simulator
      • By: Michael Westergaard, Lars m. Kristensen

[PN] Session 2

  • From 15h30 to 16h30, durand
  • Chair: Rudiger Valk
  • Paper list:
    • Decidability Results For Restricted Models of Petri Nets With Name Creation And Replication
      • By: Fernando Rosa-Velardo, David de Frutos-Escrig
    • Pomset Semantics of Finite Step Transition Systems
      • By: Jean Fanchon, Rémi Morin

[PN] Tools Demonstration

  • From 16h30 to 18h00
  • Chair:
  • Details are available here

[RSP] Session 1: Formal Methods, Synthesis & Quality Assurance

  • From 10h30 to 12h30, astier
  • Chair: Didier Buchs
  • Paper list:
    • An Experimental Model-Based Rapid Prototyping Environment For High-Confidence Embedded Software
      • By: Joseph Porter, Peter Volgyesi, Nicholas Kottenstette, Harmon Nine, Gabor Karsai And Janos Sztipanovi
    • Wolfram-a Word Level Framework For Formal Verification
      • By: Andre Suelflow, Ulrich Kuehne, Goerschwin Fey, Daniel Grosse And Rolf Drechsler
    • Rapid-Prototyping of Adaptive Component-Based Systems Using Runtime Aspectual Interactions
      • By: Kamel Barkaoui, Manru Liu And Nasredding Aoumeur
    • Adapting Models to Model Checkers, a Case Study : Analysing Aadl Using Coloured or Timed Petri Nets
      • By: Jerome Hugues, Xavier Renault And Fabrice Kordon
    • Formal Method For Rapid Soc Prototyping
      • By: Christos Pavlatos, Alexandros Dimopoulos And George Papakonstantinou

[RSP] Session 2: Communication Aspects

  • From 15h30 to 17h30, astier
  • Chair: Antônio Augusto Froehlich
  • Paper list:
    • A Flexible And Scalable Fpga Prototype Platform For rw Channel Development
      • By: Bhasker Reddy Jakka, Dillip Dash, Caner Yalcin, ly Dang, Omar Mire And Aldo Cometti
    • Synthesis of Communication Mechanisms For Multi-Tile Systems Based on Heterogeneous Multi-Processor System-On-Chips
      • By: Alexandre Chagoya-Garzon, Xavier Guerin, Frederic Rousseau, Frederic Petrot, Davide Rossetti, Alessa
    • Efficient Heuristics For Minimizing Communication Overhead in Noc-Based Heterogeneous Mpsoc Platforms
      • By: Amit Singh, wu Jigang, Alok Prakash And Thambipillai Srikanthan
    • Communication-Aware Hierarchical Online-Placement in Heterogeneous Reconfigurable Systems
      • By: Sven Schneider, Andre Meisel And Wolfram Hardt
    • Testing of an Fpga Based C2c-Communication Prototype With a Model Based Traffic Generation
      • By: Oliver Sander, Benjamin Glas, Christoph Roth, Juergen Becker And Klaus Mueller-Glaser

25 juin 2009

8h00
9h00
10h00
11h00
12h00
13h00
14h00
15h00
16h00
17h00
18h00
Break
Lunch
Keynote
Grzegorz Rozenberg

Break
Keynote
Gabriel Juhas

PN
Session 3

Session 4

RSP
Session 3: Prototyping...

Session 4: Hardware...

From 18h00 to 20h30: Visit of The Architecture Museum(Palais de Chaillot).

From 21h00 to 23h55: Banquet Dinner.

Reaction Systems: a Formal Framework For Processes Based on Biochemical Reactions

  • From 14h00 to 15h00, durand
  • Speaker: Grzegorz Rozenberg
  • The functioning of a living cell consists of a huge number of individual reactions that interact with each other. These reactions are regulated, and the two main regulation mechanisms are facilitation/acceleration and inhibition/retardation. The interaction between individual biochemical reactions takes place through their influence on each other, and this influence happens through the two mechanisms mentioned above.

    In our lecture we present a formal framework for the investigation of biochemical reactions - it is based on reaction systems. We motivate this framework by explicitely stating a number of assumptions/axioms that (we believe) hold for a great number of biochemical reactions - we point out that these assumptions are very different from the ones underlying traditional models of computation such as Petri Nets. We discuss some basic properties of reaction systems, and demonstrate how to capture and analyze, in our formal framework, some biochemistry related notions.

    The lecture is of a tutorial character and self-contained.

Unifying Petri Net Semantics With Token Flows

  • From 9h00 to 10h00, durand
  • Speaker: Gabriel Juhas
  • In the talk we advocate a unifying technique for description of different variants of semantics of Petri nets. The semantics, i.e. a behaviour is basically a set of node-labelled and arc-labelled directed acyclic graphs, called token flows, where the graphs are distinguished up to isomorphism.

    The nodes of a token flow represent occurrences of transitions of the underlying net, so they are labelled by transitions. Arcs are labelled by multisets of places. Namelly, an arc between an occurrence x of a transition a and an occurrence y of a transition b is labelled by a multiset of places, saying how many tokens produced by the occurrence x of the transition a is consumed by the occurrence y of the transition b. We show that the most prominent semantics of Petri nets, namely processes of Goltz and Reisig, partial languages of Petri nets introduced by Grabowski, rewriting terms of Meseguer and Montanari, step sequences as well as classical occurrence (firing) sequences correspond to different subsets of token flows.

    Finally, we discuss the results achieved using token flows during the last four years, including polynomial test for the acceptance of a partial word by a Petri net, synthesis of Petri nets from partial languages and token flow unfolding.

[PN] Session 3

  • From 10h30 to 12h20, durand
  • Chair: Ekkart Kindler
  • Paper list:
    • Deficiency Zero Petri Nets And Product Form
      • By: Jean Mairesse, Hoang Thach Nguyen
    • Bisimilarity Minimization in O(M Log n) Time
      • By: Antti Valmari
    • P-Semiflow Computation With Decision Diagrams
      • By: Gianfranco Ciardo, Galen Mecham, Emmanuel Paviot-Adet, Min Wan
    • Dssz-Mc-a Tool For Symbolic Analysis of Extended Petri Nets
      • By: Monika Heiner, Martin Schwarick, Alexej Tovchigrechko

[PN] Session 4

  • From 15h30 to 17h00, durand
  • Chair: Gabriel Juhas
  • Paper list:
    • Orthomodular Lattices in Occurrence Nets
      • By: Luca Bernardinello, Lucia Pomello, Stefania Rombolà
    • Hasse Diagram Generators And Petri Nets
      • By: Mateus Oliveira
    • Modeling And Analysis of Transportation Networks Using Batches Petri Nets With Controllable Batch Speed: a Case Study
      • By: Isabel Demongodin

[RSP] Session 3: Prototyping Methodology

  • From 10h30 to 12h30, astier
  • Chair: Vincent Olive
  • Paper list:
    • Operating System Support For Difference-Based Partial Hardware Reconfiguration
      • By: Tiago de a. Reis And Antonio Augusto Frohlich
    • A Methodology For Rapid Optimization of Handelc Specifications
      • By: Joseph Libby And Kenneth Kent
    • High-Level System Modeling For Rapid Hw/Sw Architecture Exploration
      • By: Chafic Jaber, Andreas Kanstein, Ludovic Apvrille, Amer Baghdadi, Patricia le Moenner And Renaud Paca
    • Rapid Prototyping Projection Algorithms With Fpga Technology
      • By: John Cole, Larry Garey And Kenneth Kent
    • Automatic Code Generation From Real-Time Systems Specifications
      • By: Laura Carnevali, Dario D'amico, Lorenzo Ridi And Enrico Vicario

[RSP] Session 4: Hardware Modeling

  • From 15h30 to 17h00, astier
  • Chair: Kenneth Kent
  • Paper list:
    • Generating an Efficient Instruction Set Simulator From a Complete Property Suite
      • By: Ulrich Kuehne, Sven Beyer And Christian Pichler
    • A Generic Instruction Set Simulator Api For Timed And Untimed Simulation And Debug of Mp2-Socs
      • By: Nicolas Pouillon, Alexandre Becoulet, Aline Vieira de Mello, Francois Pecheux And Alain Greiner
    • Configuration Measurement For Fpga-Based Trusted Platforms
      • By: Benjamin Glas, Alexander Klimm, Klaus Mueller-Glaser And Juergen Becker
    • Rapid Prototyping of Asip-Based Flexible Mmse-Ic Linear Equalizer
      • By: Atif Raza Jafri, Amer Baghdadi And Michel Jezequel

26 juin 2009

8h00
9h00
10h00
11h00
12h00
13h00
14h00
15h00
16h00
17h00
18h00
Keynote
Bill Tonti

Break
Lunch
Closing Session
Break
PN
Session 5

Session 6

RSP
Session 5: Performance...

Session 6: Automotive...

Rapid System Deployment Using The IEEE Technology Navigator: With Application to E-Fuse Design And Reliability

  • From 09h00 to 10h00, durand
  • Speaker: Bill Tonti
  • he IEEE Technology Navigator is an easy to use tool that allows a user to search through its entire digital library. At the top level a simple set of industry sectors are used to drill down into desired technical content. This engine may be used to identify pertinent literature associated with the prototyping of any element or system.

    As an example the electronic fuse (e-Fuse) can be studied in terms of intrinsic reliability and its broad use in microelectronic customization for application specific products such as on the fly self assembly or secure data transaction validation.

    The Navigator will identify material to assist in identifying a semiconductor e-Fuse prototype that results in first time right. Almost all e-Fuse designs are one time programmable and are limited to "one chance" programmable. A polycide e-Fuse technology describing the design philosophy, electrical programming, characterization, the physics of failure, and some of the many applications an on chip programmable element provides will be discussed using IEEE Technology Navigation.

[PN] Session 5

  • From 10h30 to 12h10, durand
  • Chair: Kees Van Hee
  • Paper list:
    • Oclets-Scenario-Based Modeling With Petri Nets
      • By: Dirk Fahland
    • Modelling Distributed Workflow Management Systems With Algebraic Object Nets
      • By: Michael Köhler-Bußmeier
    • Workcraft-a Framework For Interpreted Graph Models
      • By: Ivan Poliakov, Victor Khomenko, Alex Yakovlev
    • Pdetool: a Multi-Formalism Modeling Tool For Discrete-Event Systems Based on Sdes Description
      • By: Amir Jalaly Bidgoly, Ali Khalili, Mohammad Abdollahi Azgomi

[PN] Session 6

  • From 14h00 to 15h00, durand
  • Chair: Karsten Wolf
  • Paper list:
    • Monotonicity in Service Orchestrations
      • By: Anne Bouillard, Sidney Rosario, Albert Benveniste, Stefan Haar
    • Compositional Service Trees
      • By: Wil Van Der Aalst, Kees Van Hee, Peter Massuthe, Natalia Sidorova, Jan Martijn Van Der Werf

[RSP] Session 5: Performance Optimization

  • From 10h30 to 12h30, astier
  • Chair: Frédéric Pétrot
  • Paper list:
    • High-Performance Buffer Mapping to Exploit Dram Concurrency in Multiprocessor Dsp Systems
      • By: Dongwon Lee, Shuvra Bhattacharyya And Wayne Wolf
    • Area-Time Estimation of Controller For Porting C-Based Functions Onto Fpga
      • By: My Chuong Lieu, Siew Kei Lam And Thambipillai Srikanthan
    • Instruction Cache Tuning For Embedded Multitasking Applications
      • By: Santanu Kumar Dash And Srikanthan Thambipillai
    • Efficient Data Access Management For Fpga-Based Image Processing Socs
      • By: Zahir Larabi, Yves Mathieu And Stephane Mancini
    • Design And Implementation of an Uwb Digital Transmitter Based on The Multiband Ofdm Physical Layer Proposal
      • By: Michalis Platsis, Ioannis Papaefstathiou And Dimitrios Meintanis

[RSP] Session 6: Automotive & Industrial Applications

  • From 13h30 to 15h00, astier
  • Chair: Wolfram Hardt
  • Paper list:
    • Physical Layer Extraction of Flexray Configuration Parameters
      • By: Matthias Heinz, Verena Hess And Klaus Mueller-Glaser
    • An Interactive Approach to Timing Accurate Pci-X Simulation
      • By: Russell Tessier, Kevin Andryc And Patrick Kelly
    • An Approach to Supply Simulations of The Functional Environment of Ecus For Hardware-In-The-Loop Test Systems Based on Ee-Architectures Conform to Autosar
      • By: Martin Hillenbrand And Klaus Mueller-Glaser
    • Fpga-Based Radar Signal Processing For Automotive Driver Assistance System
      • By: Jean Saad, Amer Baghadadi And Frantz Bodereau