The Community for Technology Leaders
Formal Methods and Models for Co-Design, ACM/IEEE International Conference on (2003)
Mont Saint-Michel, France
June 24, 2003 to June 26, 2003
ISBN: 0-7695-1923-7
TABLE OF CONTENTS
Introduction
Opening Remarks

null (PDF)

pp. null
Conference Updates

null (PDF)

pp. null
Invited Talk
System Level Models and Co-design

null (PDF)

pp. null

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

Anik? Costa , Universidade Nova de Lisboa, Faculdade de Ci?ncias e Tecnologia, Dep. of Elect. Eng.
Lu?s Gomes , Universidade Nova de Lisboa, Faculdade de Ci?ncias e Tecnologia, Dep. of Elect. Eng.
pp. 24
Short Presentation Session

null (PDF)

pp. 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)

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)

Florian Kammller , Institut fur Softwaretechnik und Theoretische Informatik
Margot Bittner , 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 (PDF)

pp. null

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

Dong Wang , Carnegie Mellon Univ.
Edmund Clarke , Carnegie Mellon Univ.
Muralidhar Talupur , Carnegie Mellon Univ.
Orna Grumberg , TECHNION
pp. 55
Field Modifiability and Verifiability

null (PDF)

pp. null
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
Refinement/Conformance I

null (PDF)

pp. null

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

Francoise Bellegarde , Univ. Franche-Comte
Olga Kouchnarenko , Univ. Franche-Comte
Celina Charlet , Univ. Franche-Comte
pp. 103

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

Gerard Postuma , Philips Semiconductors, Chief Technology Office - Design Technology Group
Nick Gatherer , Philips Semiconductors, Chief Technology Office - Design Technology Group
Marleen Boonen , Philips Semiconductors, Chief Technology Office - Design Technology Group
Jos Verhaegh , Philips Semiconductors, Chief Technology Office - Design Technology Group
Thierry J-F. Omnes , Philips Semiconductors, Chief Technology Office - Design Technology Group
pp. 113
Invited Talk
Validation, Co-validation

null (PDF)

pp. null

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

Andrea Fedeli , STMicroelectronics
Umberto Rossi , STMicroelectronics
Franco Toto , STMicroelectronics
Franco Fummi , Universita di Verona
Graziano Pravadelli , Universita di Verona
pp. 145

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

Klaus Schneider , University of Kaiserslautern, Department of Computer Science, Reactive Systems Group
Tobias Sch? , University of Kaiserslautern, Department of Computer Science, Reactive Systems Group
pp. 153

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

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

Paulo R. M. Maciel , Universidade Federal de Pernambuco
S?rgio M.M. Fernandes , Universidade Cat?lica de Pernambuco
pp. 172
Invited Talk

Modular Hierarchies of Models for Embedded Systems (Abstract)

Manfred BROY , Institut f?r Informatik, Technische Universit?t M?nchen
pp. 183
Refinement II

null (PDF)

pp. null
Synthesis, Optimization

null (PDF)

pp. null

A Generalised Approach to Supervisor Synthesis (Abstract)

Roberto Ziller , University of Karlsruhe
Klaus Schneider , University of Kaiserslautern
pp. 217

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

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
Invited Talk
Formal Verification II

null (PDF)

pp. null

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

Krzysztof Worytkiewicz , 2 av. des Planches
Christoph Sprenger , Projet Lemme, INRIA Sophia Antipolis
pp. 255

Verification of Control Properties in the Polyhedral Model (Abstract)

Katell Morin-Allory , IRISA, Campus de Beaulieu
David Cachera , IRISA, Campus de Beaulieu
pp. 265
Panel II

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

Rajesh Gupta , University of California at San Diego
Sandeep Shukla , Virginia Polytechnic and State University
pp. 277
Closing Talk
Author Index

Author Index (PDF)

pp. 285
88 ms
(Ver 3.1 (10032016))