Message from the Chairs

Committee Members and Organizers (PDF)

pp. x

Opening Remarks

null

Conference Updates

null

Invited Talk

Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design (Abstract)

Jose Meseguer, University of Illinois at Urbana-Champaign

pp. 3

PDF

System Level Models and Co-design

null

MoDe: A Method for System-Level Architecture Evaluation (Abstract)

Jan Romberg, TU M?nchen

Oscar Slotosch Gabor Hahn, Lichtenbergstr. 8

pp. 13

PDF

From Use Cases to System Implementation: Statechart Based Co-design (Abstract)

Lu?s Gomes, Universidade Nova de Lisboa, Faculdade de Ci?ncias e Tecnologia, Dep. of Elect. Eng.

Anik? Costa, Universidade Nova de Lisboa, Faculdade de Ci?ncias e Tecnologia, Dep. of Elect. Eng.

pp. 24

PDF

Julio A. de Oliveira Filho

Petri Net Based Interface Analysis for Fast IP-Core Integration (Abstract)

Manoel E. de Lima

Paulo Romero Maciel

pp. 34

PDF

Short Presentation Session

null

Goal-Oriented Requirements Analysis for Process Control Systems Design (PDF)

Islam El-Maddah, Department of Computer Science, King?s College London, London WC2R 2LS, UK

Tom Maibaum, Department of Computer Science, King?s College London, London WC2R 2LS, UK

pp. 45

Analyzing Concurrency in Computational Networks (PDF)

Sander Stuijk

Twan Basten, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, The Netherlands.

pp. 47

Translating Fusion/UML to Object-Z (PDF)

Margot Bittner, Institut fur Softwaretechnik und Theoretische Informatik

Florian Kammller, Institut fur Softwaretechnik und Theoretische Informatik

pp. 49

Finding Good Counter-Examples to Aid Design Verification (PDF)

Goerschwin Fey, Institute of Computer Science, University of Bremen, 28359 Bremen, Germany

Rolf Drechsler, Institute of Computer Science, University of Bremen, 28359 Bremen, Germany

pp. 51

Formal Verification I

null

High Level Verification of Control Intensive Systems Using Predicate Abstraction (Abstract)

Edmund Clarke, Carnegie Mellon Univ.

Orna Grumberg, TECHNION

Muralidhar Talupur, Carnegie Mellon Univ.

Dong Wang, Carnegie Mellon Univ.

pp. 55

PDF

Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions (Abstract)

Sudarshan K. Srinivasan, Georgia Institute of Technology, Atlanta

Miroslav N. Velev, Georgia Institute of Technology, Atlanta

pp. 65

PDF

Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs (Abstract)

Magali Contensin, CMI/Universite

Laurence Pierre, I3S - Universite de Nice

pp. 75

PDF

Field Modifiability and Verifiability

null

Engineering Changes in Field Modifiable Architectures (Abstract)

pp. 87

PDF

Panel I

Hierarchical and Incremental Verification for System Level Design: Challenges and Accomplishments (Abstract)

Grant Martin, Cadence Berkeley Labs

Sandeep Shukla, Virginia Polytechnic and State University

pp. 97

PDF

Refinement/Conformance I

null

How to Compute the Refinement Relation for Parameterized Systems (Abstract)

Francoise Bellegarde, Univ. Franche-Comte

Celina Charlet, Univ. Franche-Comte

Olga Kouchnarenko, Univ. Franche-Comte

pp. 103

PDF

Using SSDE for USB2.0 conformance co-verification (Abstract)

Thierry J-F. Omnes, Philips Semiconductors, Chief Technology Office - Design Technology Group

Gerard Postuma, Philips Semiconductors, Chief Technology Office - Design Technology Group

Jos Verhaegh, Philips Semiconductors, Chief Technology Office - Design Technology Group

Marleen Boonen, Philips Semiconductors, Chief Technology Office - Design Technology Group

Nick Gatherer, Philips Semiconductors, Chief Technology Office - Design Technology Group

pp. 113

PDF

From Algorithm and Architecture Specifications to Automatic Generation of Distributed Real-Time Executives: a Seamless Flow of Graphs Transformations (Abstract)

Thierry Grandpierre, ESIEE Paris, Cite Descarte BP99

Yves Sorel, INRIA, Domaine de Voluceau BP 105

pp. 123

PDF

Methods for exploiting SAT solvers in unbounded model checking (Abstract)

K. L. McMillan, Cadence Berkeley Labs

pp. 135

PDF

Validation, Co-validation

null

On the Use of a High-Level Fault Model to Check Properties Incompleteness (Abstract)

Franco Fummi, Universita di Verona

Graziano Pravadelli, Universita di Verona

Andrea Fedeli, STMicroelectronics

Umberto Rossi, STMicroelectronics

Franco Toto, STMicroelectronics

pp. 145

PDF

Exact Runtime Analysis Using Automata-Based Symbolic Simulation (Abstract)

Tobias Sch?, University of Kaiserslautern, Department of Computer Science, Reactive Systems Group

Klaus Schneider, University of Kaiserslautern, Department of Computer Science, Reactive Systems Group

pp. 153

PDF

Real-time Property Preservation in Approximations of Timed Systems (Abstract)

Jinfeng Huang, Eindhoven University of Technology

Jeroen Voeten, Eindhoven University of Technology

Marc Geilen, Eindhoven University of Technology

pp. 163

PDF

Reliability Evaluation for Dependable Embedded System Specifications: An Approach Based on DSPN (Abstract)

S?rgio M.M. Fernandes, Universidade Cat?lica de Pernambuco

Paulo R. M. Maciel, Universidade Federal de Pernambuco

pp. 172

PDF

Modular Hierarchies of Models for Embedded Systems (Abstract)

Manfred BROY, Institut f?r Informatik, Technische Universit?t M?nchen

pp. 183

PDF

Refinement II

null

Verification of Transaction-Level SystemC models using RTL Testbenches (Abstract)

pp. 199

PDF

LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect (Abstract)

Pierre Wodey, ISIMA - LIMOS

Geoffrey Camarroque, ISIMA - LIMOS

Fabrice Baray, ISIMA - LIMOS

Richard Hersemeule, STMicrolectronics

Jean-Philippe Cousin, STMicrolectronics

pp. 204

PDF

Synthesis, Optimization

null

A Generalised Approach to Supervisor Synthesis (Abstract)

Roberto Ziller, University of Karlsruhe

Klaus Schneider, University of Kaiserslautern

pp. 217

PDF

Optimizations for Faster Execution of Esterel Programs (Abstract)

Dumitru Potop-Butucaru, Ecole des Mines de Paris, CMA

Robert de Simone, INRIA Sophia Antipolis

pp. 227

PDF

Bridging CSP and C++ with Selective Formalism and Executable Specifications (Abstract)

W. B. Gardner, Dept. of Computing & Information Science, Univ. of Guelph, Guelph, Ontario, Canada

pp. 237

PDF

Bluespec: A language for hardware design, simulation, synthesis and verification Invited Talk (Abstract)

Arvind, Massachusetts Institute of Technology

pp. 249

PDF

Formal Verification II

null

A Verification Methodology for Infinite-State Message Passing Systems (Abstract)

Christoph Sprenger, Projet Lemme, INRIA Sophia Antipolis

Krzysztof Worytkiewicz, 2 av. des Planches

pp. 255

PDF

Verification of Control Properties in the Polyhedral Model (Abstract)

David Cachera, IRISA, Campus de Beaulieu

Katell Morin-Allory, IRISA, Campus de Beaulieu

pp. 265

PDF

PANEL: Should the space of implementation possibilities be determined by the abilities of high-level synthesis and validation? (Abstract)

Panel II

Rajesh Gupta, University of California at San Diego

Sandeep Shukla, Virginia Polytechnic and State University

pp. 277

PDF

Closing Talk

Robust System Design with Uncertain Information (PDF)

Giovanni De Micheli, Stanford University

pp. 283

Author Index

Author Index (PDF)

pp. 285