Message from the Conference Chairs

ACSD 2003 Organization (PDF)

pp. x

Program Committee (PDF)

pp. xi

Additional Reviewers (PDF)

pp. xii

Invited Papers

The Reality of System Design Today: Do Theory and Practice Meet? (PDF)

Grant Martin, Cadence Design Systems

pp. 3

Cyclic Communicating Processes: Hierarchy and Verification (PDF)

P. S. Thiagarajan, National University of Singapore

pp. 4

Model Driven Embedded Systems (PDF)

Ian Oliver, Nokia Research Center

pp. 5

Polychrony for Formal Refinement-Checking in a System-Level Design Methodology (PDF)

Regular Papers

Jean-Pierre Talpin, INRIA/IRISA

Paul Le Guernic, INRIA/IRISA

Sandeep Kumar Shukla, Virginia Tech

Rajesh Gupta, University of California at San Diego

Frédéric Doucet, University of California at San Diego

pp. 9

Case Studies of Model Checking for Embedded System Designs (Abstract)

Xi Chen, University of California at Riverside

Harry Hsieh, University of California at Riverside

Felice Balarin, Cadence Berkeley Laboratories

Yosinori Watanabe, Cadence Berkeley Laboratories

pp. 20

PDF

Quasi-Static Scheduling for Concurrent Architectures (Abstract)

Jordi Cortadella, Universitat Politècnica de Catalunya

Alex Kondratyev, Cadence Berkeley Labs

Luciano Lavagno, Politecnico di Torino

Yosinori Watanabe, Cadence Berkeley Labs

pp. 29

PDF

Synthesis of Open Reactive Systems from Scenario-Based Specifications (Abstract)

Yves Bontemps, University of Namur

Pierre-Yves Schobbens, University of Namur

pp. 41

PDF

Detecting State Coding Conflicts in STG Unfoldings Using SAT (Abstract)

Victor Khomenko, University of Newcastle upon Tyne

Maciej Koutny, University of Newcastle upon Tyne

Alex Yakovlev, University of Newcastle upon Tyne

pp. 51

PDF

A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs (Abstract)

Javier Esparza, University of Stuttgart

pp. 61

PDF

Separation of Concerns in the Formal Design of Real-Time Shared Data-Space Systems (Abstract)

Mohammad Reza Mousavi, Eindhoven University of Technology

Michel Reniers, Eindhoven University of Technology

Twan Basten, Eindhoven University of Technology

Michel Chaudron, Eindhoven University of Technology

pp. 71

PDF

Modelling a Secure, Mobile, and Transactional System with CO-OPN (Abstract)

Didier Buchs, Swiss Federal Institute of Technology Lausanne

Stanislav Chachkov, Swiss Federal Institute of Technology Lausanne

David Hurzeler, Swiss Federal Institute of Technology Lausanne

pp. 82

PDF

Developing a Formal Specification for the Mission System of a Maritime Surveillance Aircraft (Abstract)

Laure Petrucci, ENS de Cachan

Jonathan Billington, University of South Australia

Lars M. Kristensen, University of Aarhus

Zahid H. Qureshi, Defence Science and Technology Organisation

pp. 92

PDF

Design Validation of ZCSP with SPIN (Abstract)

Vincent Beaudenon, UPMC - LIP6 - ASIM

Emmanuelle Encrenaz, UPMC - LIP6 - ASIM

Jean-Lou Desbarbieux, UPMC - LIP6 - ASIM

pp. 102

PDF

Memory Fault Tolerance Software Mechanisms: Design and Configuration Support through SWN Models (Abstract)

P. Ballarini, Università di Torino

L. Capra, Univeristà di Milano

G. Franceschinis, Univeristà Piemonte Orientale

M. De Pierro, Univeristà Piemonte Orientale

pp. 111

PDF

Component-Based Design: Towards Guided Composition (Abstract)

S. Moschoyiannis, University of Surrey

M. W. Shields, University of Surrey

pp. 122

PDF

Compositional High Level Petri Nets with Timing Constraints — A Comparison (Abstract)

Elisabeth Pelz, Universit? Paris XII-Val de Marne

Hans Fleischhack, CvO Universit?t Oldenburg

pp. 132

PDF

Compositional Verification of Integrity for Digital Stream Signature Protocols (Abstract)

Roberto Gorrieri, Università di Bologna

Fabio Martinelli, Istituto di Informatica e Telematica - C.N.R.

Marinella Petrocchi, Istituto di Informatica e Telematica - C.N.R.

Anna Vaccarelli, Istituto di Informatica e Telematica - C.N.R.

pp. 142

PDF

Merging State-Based and Action-Based Verification (Abstract)

Henri Hansen, Tampere University of Technology

Heikki Virtanen, Tampere University of Technology

Antti Valmari, Tampere University of Technology

pp. 150

PDF

Communicating Transaction Processes (Abstract)

Abhik Roychoudhury, National University of Singapore

P. S. Thiagarajan, National University of Singapore

pp. 157

PDF

Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions (Abstract)

Adrianna Alexander, Humboldt-Universit?t zu Berlin

Wolfgang Reisig, Humboldt-Universit?t zu Berlin

pp. 167

PDF

Modifying Petri Net Models by Means of Crosscutting Operations (Abstract)

João Paulo Barros, Universidade Nova de Lisboa and Instituto Politécnico de Beja

Luís Gomes, Universidade Nova de Lisboa

pp. 177

PDF

Specification Coverage Aided Test Selection (Abstract)

Tuomo Pyhälä, Helsinki University of Technology

Keijo Heljanko, Helsinki University of Technology

pp. 187

PDF

Verification of JavaSpaces™ Parallel Programs (Abstract)

Jaco van de Pol, Centrum voor Wiskunde en Informatica

Miguel Valero Espada, Centrum voor Wiskunde en Informatica

pp. 196

PDF

On Lifting of Statechart Structuring Mechanisms (Abstract)

Lu? Gomes, Universidade Nova de Lisboa and UNINOVA, Centro de Rob?tica Inteligente

Anik? Costa, Universidade Nova de Lisboa and UNINOVA, Centro de Rob?tica Inteligente

pp. 206

PDF

A New Synchronization in Finite Stochastic Petri Box Calculus (Abstract)

Hermenegilda Macià, Universidad de Castilla-La Mancha

Valentín Valero, Universidad de Castilla-La Mancha

Fernando Cuartero, Universidad de Castilla-La Mancha

Fernando L. Pelayo, Universidad de Castilla-La Mancha

pp. 216

PDF

Tool Presentations

C-Sim version 5.0 (PDF)

Roman Jokl, University of West Bohemia in Pilsen

Stanislav Racek, University of West Bohemia in Pilsen

pp. 229

ABTOOLS: Another B Tool (PDF)

Jean-Louis Boulanger, University of Technology of Compiegne

pp. 231

Rialto Profile in the SMW Toolkit (PDF)

Dag Bj?rklund, ?bo Akademi University

Johan Lilius, ?bo Akademi University

Ivan Porres, ?bo Akademi University

pp. 233

HiWorD: A Petri Net-Based Hierarchical Workflow Designer (PDF)

Boualem Benatallah, University of New South Wales

Piotr Chrz¸stowski-Wachtel, Warsaw University and Polish-Japanese Institute of Information Technology

Rachid Hamadi, University of New South Wales

Milton O?Dell, Justwin Technologies Pty Ltd

Adi Susanto, University of New South Wales

pp. 235

CAST — A Task-Level Concurrency Analysis Tool (PDF)

Sander Stuijk, Eindhoven University of Technology

Twan Basten, Eindhoven University of Technology

Jan Ypma, Eindhoven University of Technology

pp. 237

A Framework for the Development of Protocols (PDF)

Federico Crazzolara, NEC Europe and Chi Spaces Technologies ltd.

Giuseppe Milicia, University of Aarhus and Chi Spaces Technologies ltd.

pp. 239

BHDL: Circuit Design in B (PDF)

Ammar Aljer, Laboratoire d?Informatique Fondamentale de Lille

Philippe Devienne, Laboratoire d?Informatique Fondamentale de Lille

Sophie Tison, Laboratoire d?Informatique Fondamentale de Lille

Jean-Louis Boulanger, Université de Compiègne

Georges Mariano, Institut National de Recherche sur les Transports et leur Sécurité

pp. 241

CONFRES: Interactive Coding Conflict Resolver Based on Core Visualisation (PDF)

A. Madalinski, University of Newcastle upon Tyne

pp. 243

Abstract Model Checking and Refinement of Temporal Logic in αSPIN (PDF)

María del Mar Gallardo, University of Malaga

Jesús Martínez, University of Malaga

Pedro Merino, University of Malaga

Ernesto Pimentel, University of Malaga

pp. 245

VoDkaV Tool: Model Checking for Extracting Global Scheduler Properties from Local Restrictions (PDF)

Juan José Sánchez Penas, University of Corunha

Thomas Arts, IT-University of Giöteborg

pp. 247

AutoFOCUS and the MoDe Tool (PDF)

Jan Romberg, Technical Univesität München

Jan J?rjens, Technical Univesität München

Guido Wimmel, Technical Univesität München

Oscar Slotosch, Validas AG

Gabor Hahn, Validas AG

pp. 249

Author Index

Author Index (PDF)

pp. 251