IFIP TC6 Open Digital Library

27. FORTE 2007: Tallinn, Estonia

Formal Techniques for Networked and Distributed Systems - FORTE 2007, 27th IFIP WG 6.1 International Conference, Tallinn, Estonia, June 27-29, 2007, Proceedings

John Derrick, Jüri Vain

Springer, Lecture Notes in Computer Science 4574, ISBN: 978-3-540-73195-5



Contents

Invited Talk

Contracts for BIP: Hierarchical Interaction Models for Compositional Verification.

Susanne Graf, Sophie Quinton

 1-18

Technical Session 1. Message Sequence Charts and SDL

Thread-Based Analysis of Sequence Diagrams.

Haitao Dan, Robert M. Hierons, Steve Counsell

 19-34

Recovering Repetitive Sub-functions from Observations.

Guy-Vincent Jourdan, Hasan Ural, Shen Wang, Hüsnü Yenigün

 35-49

Specification of Timed EFSM Fault Models in SDL.

Samrat S. Batth, Elisangela Rodrigues Vieira, Ana R. Cavalli, M. Ümit Uyar

 50-65

Technical Session 2. Concurrency

Coordination Via Types in an Event-Based Framework.

GianLuigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto

 66-80

Exploring the Connection of Choreography and Orchestration with Exception Handling and Finalization/Compensation.

Hongli Yang, Xiangpeng Zhao, Chao Cai, Zongyan Qiu

 81-96

Towards Modal Logic Formalization of Role-Based Access Control with Object Classes.

Junghwa Chae

 97-111

Technical Session 3. Model Programs

State Isomorphism in Model Programs with Abstract Data Structures.

Margus Veanes, Juhan P. Ernits, Colin Campbell

 112-127

Composition of Model Programs.

Margus Veanes, Colin Campbell, Wolfram Schulte

 128-142

Technical Session 4. Theory

New Bisimulation Semantics for Distributed Systems.

David de Frutos-Escrig, Fernando Rosa-Velardo, Carlos Gregorio-Rodríguez

 143-159

Event Correlation with Boxed Pomsets.

Thomas Gazagnaire, Loïc Hélouët

 160-176

A Simple Positive Flows Computation Algorithm for a Large Subclass of Colored Nets.

Sami Evangelista, Christophe Pajault, Jean-François Pradat-Peyre

 177-195

Technical Session 5. Verification

Improvements for the Symbolic Verification of Timed Automata.

Rongjie Yan, Guangyuan Li, Wenliang Zhang, Yunquan Peng

 196-210

The DHCP Failover Protocol: A Formal Perspective.

Rui Fan, Ralph E. Droms, Nancy D. Griffeth, Nancy A. Lynch

 211-226

Verifying Erlang/OTP Components in mu CRL.

Qiang Guo

 227-246

Technical Session 6. Model Checking

Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata.

Fei He, Luciano Baresi, Carlo Ghezzi, Paola Spoletini

 247-262

Testing Distributed Systems Through Symbolic Model Checking.

Gabriel Kalyon, Thierry Massart, Cédric Meuter, Laurent Van Begin

 263-279

An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets.

Kais Klai, Laure Petrucci, Michel A. Reniers

 280-295

Technical Session 7. Requirements and QoS

Identifying Acceptable Common Proposals for Handling Inconsistent Software Requirements.

Kedian Mu, Zhi Jin

 296-308

Formalization of Network Quality-of-Service Requirements.

Christian Webel, Reinhard Gotzhein

 309-324

Technical Session 8. Components

Robustness in Interaction Systems.

Mila E. Majster-Cederbaum, Moritz Martens

 325-340

Transactional Reduction of Component Compositions.

Serge Haddad, Pascal Poizat

 341-357

Specifying and Composing Interaction Protocols for Service-Oriented System Modelling.

João Abreu, Laura Bocchi, José Luiz Fiadeiro, Antónia Lopes

 358-373