|
|
Day One
|
Time
|
Event
|
Chair
|
| 8:30 -9:00 |
Opening
Remarks: Rajesh Gupta
Conference
updates: Jean-Pierre Talpin and Sandeep K. Shukla
|
- |
| 9:00-10:00 |
Invited
Talk: Jose Meseguer
University
of Illinois at Urbana Champagne, USA
Executable
Computational Logics: Combining Formal Methods and Programming Language
Based System Design
|
Paul Le Guernic
IRISA, France |
| 10:00-10:30 |
Coffee
|
|
| 10:30-11:30 |
Invited Talk: Manfred
Broy
Technical University of Munich,
Germany
Modular Hierarchies of Models
for Embedded Systems |
Zebo
Peng
Linkoeping University, Sweden |
| 11:30-12:00 |
MoDe:
A Method for System-Level Architecture Evaluation,Jan Romberg,
Oscar Slotosch, Gabor Hahn
|
|
|
|
|
|
|
|
| 12:00-1:30 |
Lunch
|
|
| 1:30-2:30 |
Short Presentation
Session |
Hans Eveking
University of Darmstadt, Germany |
|
Goal-Oriented
Requirements Analysis for Process Control Systems Design,Islam
Ahmed El-Maddah, Tom Maibuam
|
|
|
Analyzing
Concurrency in Computational Networks, Sander Stuijk, Twan Basten
|
|
|
Translating
Fusion/UML to Object-Z, Margot Bittner, Florian Kammueller
|
|
|
Finding
Good Counter-Examples to Aid Design Verification, Görschwin
Fey, Rolf Drechsler
|
|
| 2:30-4:00 |
Session: Formal
Verification I |
Ken
McMillan
Cadence Laboratories, USA |
|
High
Level Verification for Control Intensive Systems Using Predicate Abstraction,
Edmund Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
|
|
|
Formal
Verification of an Intel XScale Processor Model with Scoreboarding,Specialized
Execution Pipelines, and Imprecise Data-Memory Exceptions, Sudarshan
K. Srinivasan, Miroslav N. Velev
|
|
|
Combining
Acl2 and a nu-calculus model-checker to verify system-level designs, Magali
Contensin, Laurence Pierre
|
|
| 4:00-4:30 |
Coffee
|
|
| 4:30-5:00 |
Field Modifiability
and Verifiability |
Forest Brewer
University of California, Santa
Barbara, USA |
|
Engineering
Changes in Field Modifiable Architectures, Hiroshi Saito, Kenshu
Seto, Yoshihisa Kojima, Satoshi Komatsu, Masahiro Fujita
|
|
| 5:00-7:00 |
Panel I:
Hierarchical and Incremental Verification for System Level Design:
Challenges and Accomplishments,
Marten van Hulst (Philips), Franco
Fummi (Verona), Forest Brewer (Santa Barbara), Hans Eveking (Darmstadt),
Constance Heitmeyer (NRL) |
Grant
Martin
Cadence Laboratories, USA |
| |
Day Two
|
|
|
Time
|
Event
|
Chair
|
| 9:00-10:30 |
Session: Refinement/Conformance
I |
Manfred Broy
Technical Univeristy of Meunchen,
Germany
|
|
How
to Compute the Refinement Relation for Parameterized Systems, Francoise
Belegarde, Célina Charlet, Olga Kouchnarenko
|
|
|
Using
SSDE for USB2.0 conformance co-verification, Thierry Omnes, Gerard
Postuma, Jos Verhaegh, Marleen Boonen, Nick Gatherer
|
|
|
From
High Level Graph Specification of Algorithm and Architecture to the Automatic
Generation of Distributed Executive, Thierry Grandpierre, Yves Sorel
|
|
| 10:30-11:00 |
Coffee
|
|
| 11:00-12:00 |
Invited
Talk: Ken McMillan,
Cadence Labs, USA
Title T.B.A. |
Connie Heitmeyer
Naval Research Labs, USA |
| 12:00-1:30 |
Lunch
|
|
| 1:30-3:30 |
Session: Validation,
Co-Validation |
Jose Meseguer
University of Ilinois
at Urbana Champagne
|
|
On
the use of a high-level fault model to check properties incompleteness,
Franco Fummi, Graziano Pravadelli, Andrea
Fedeli, Umberto Rossi, Franco Toto
|
|
|
Exact
Runtime Analysis Using Automata-Based Symbolic Simulation, Tobias
Schuele, Klaus Schneider
|
|
|
Real-time
Property Preservation in Approximations of Timed Systems, Jinfeng
Huang, Jeroen Voeten, Marc Geilen
|
|
|
Reliability
Evaluation for Dependable Embedded Systems, Sérgio Murilo
Maciel Fernandes, Paulo Romero Martins Macie
|
|
| 3:30-4:00 |
Coffee
|
|
| 4:00-5:00 |
Session:
Co-Design & IP-integration
Use Cases to System Implementation: State Chart Based
Co-Design, Luis Gomes, Aniko Costa
Petrinet Based Interface Analysis for Fast IP Integration,
Julio Alexandrino de Oliveira Filho, Manuel Eusébio de Lima,
Paulo Romero Maciel
|
Arvind
MIT
|
| 5:00-6:00 |
Session: Refinement
II |
Martin Van Hulst Philips
Research, The Netherlands |
|
Verification
of Transaction Level Models in SystemC using RTL Test benches, Rohit
Jindal, Kshitiz Jain
|
|
|
LOTOS
Code generation for STBUS Based SOC Model Checking, Pierre Wodey,
Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Philippe Cousin
|
|
|
|
|
| |
Day Three
|
|
| 9:00-10:30 |
Session:
Synthesis, Optimization
|
Stephen Edwards Coloumbia
University, USA |
|
A
Generalized Approach to Supervisor Synthesis, Roberto Ziller, Klaus
Schneider
|
|
|
Optimizations
for Faster Execution of Esterel Programs, Dumitru Potop, Robert
de Simone
|
|
|
Bridging
CSP and C++ with Selective Formalism and Executable Specifications,
William B. Gardner
|
|
| 10:30-11:00 |
Coffee
|
|
| 11:00-12:00 |
Invited
Talk: Arvind,
Massachussets Institute of Technology,
USA
BlueSpec:
A language for hardware design, simulation, synthesis and verification |
Rajesh Gupta
University of California,
San Diego
|
| 12:00-1:30 |
Lunch
|
|
| 1:30-2:30 |
Session: Formal
Verification II |
R. K. Shyamasundar
Tata Institute, India
|
|
A
Verification Methodology for Infinite-State Message-Passing Systems, Krzysztof
Worytkiewicz, Christoph Sprenger
|
|
|
Verification
of Control Properties in the Polyhedral Model, David Cachera, Katell
Morin-Allory
|
|
| 2:30-3:00 |
Coffee
|
|
| 3:00-4:30 |
Panel
2: Should the space of implementation possibilities be determined by
the abilities of high-level
synthesis and validation? Grant
Martin (Cadence), Stephen Edwards (Columbia), Arvind (MIT), Forest
Brewer (Santa Barbara), Masahiro Fujita (Tokyo)
|
Rajesh Gupta
University of California, San
Diego, USA |
| 4:30-5:00 |
Break
|
|
| 5:00-6:00 |
Closing
Talk: Giovanni De Micheli,
Stanford University, USA
Robust system design with uncertain
information |
François
Bodin
IRISA, France |
|
