CSDL - Proceedings A

Organizing and Steering Committees (PDF)

pp. xii

Program Committee (PDF)

pp. xiii

Additional Reviewers (PDF)

pp. xiii

Participating Countries (PDF)

pp. xiv

Keynote Address (PDF)

pp. xv

Session I-A: Testing I

A New Way of Automating Statistical Testing Methods (Abstract)

S.-D. Gouraud, L.R.I., Universit? Paris-Sud

A. Denise, L.R.I., Universit? Paris-Sud

M.-C. Gaudel, L.R.I., Universit? Paris-Sud

B. Marre, L.R.I., Universit? Paris-Sud; CEA, LIST/DTSI/SLA/LSL

pp. 5

PDF

Automatic Test Data Generation for Programs with Integer and Float Variables (Abstract)

Nguyen Tran Sy, Universit? catholique de Louvain

Yves Deville, Universit? catholique de Louvain

pp. 13

PDF

TestEra: A Novel Framework for Automated Testing of Java Programs (Abstract)

Darko Marinov, MIT Laboratory for Computer Science

Sarfraz Khurshid, MIT Laboratory for Computer Science

pp. 22

PDF

Session I-B: Transformation/Construction I

Generating EDI Message Translations from Visual Specifications (Abstract)

John Grundy, University of Auckland

Rick Mugridge, University of Auckland

John Hosking, University of Auckland

Paul Kendall, Orion Systems Ltd

pp. 35

PDF

The Synthesis of a Java Card Tokenization Algorithm (Abstract)

Ewen Denney, University of Edinburgh

pp. 43

PDF

Wins and Losses of Algebraic Transformations of Software Architectures (Abstract)

H. M. Fahmy, University of Waterloo

R. C. Holt, University of Waterloo

J. R. Cordy, Queen?s University

pp. 51

PDF

Session II-A: Verification and Validation/High-Assurance Systems Acceptance-Based Assurance (Abstract)

C. O'Halloran, Systems Assurance Group

pp. 63

PDF

Specification Modeling and Validation Applied to a Family of Network Security Products (Abstract)

Robert J. Hall, AT&T Labs Research

pp. 71

PDF

Certifying Domain-Specific Policies (Abstract)

Michael Lowry, NASA Ames Research Center

Thomas Pressburger, NASA Ames Research Center

Grigore Rosu, NASA Ames Research Center

pp. 81

PDF

Automated Validation of Software Models (Abstract)

Steve Sims, Reactive Systems, Inc.

Rance Cleaveland, Reactive Systems, Inc.

Ken Butts, Ford Motor Company

Scott Ranville, New Eagle Software

pp. 91

PDF

Session II-B: Structure

Context-Aware Browsing of Large Component Repositories (Abstract)

Yunwen Ye, SRA Key Technology Laboratory, Inc; University of Colorado

Gerhard Fischer, University of Colorado

pp. 99

PDF

Identification of High-Level Concept Clones in Source Code (Abstract)

Andrian Marcus, Kent State University

Jonathan I. Maletic, Kent State University

pp. 107

PDF

Static Consistency Checking for Distributed Specifications (Abstract)

Christian Nentwich, University College London

Wolfgang Emmerich, University College London

Anthony Finkelstein, University College London

pp. 115

PDF

Session III-A: Testing II

Test Purposes: Adapting the Notion of Specification to Testing (Abstract)

Y. Ledru, Laboratoire Logiciels Syst?mes R?seaux/IMAG

L. du Bousquet, Laboratoire Logiciels Syst?mes R?seaux/IMAG

P. Bontron, Laboratoire Logiciels Syst?mes R?seaux/IMAG

O. Maury, Laboratoire Logiciels Syst?mes R?seaux/IMAG

C. Oriat, Laboratoire Logiciels Syst?mes R?seaux/IMAG

M.-L. Potet, Laboratoire Logiciels Syst?mes R?seaux/IMAG

pp. 127

PDF

Monitoring Programs Using Rewriting (Abstract)

Klaus Havelund, NASA Ames Research Center

Grigore Rosu, NASA Ames Research Center

pp. 135

PDF

Program Execution-Based Module Cohesion Measurement (Abstract)

Neelam Gupta, The University of Arizona

Praveen Rao, The University of Arizona

pp. 144

PDF

Session III-B: Transformation/Construction II

Composition and Refinement of Behavioral Specifications (Abstract)

Dusko Pavlovic, Kestrel Institute

Douglas R. Smith, Kestrel Institute

pp. 157

PDF

Instantiating and Detecting Design Patterns: Putting Bits and Pieces Together (Abstract)

Hervé Albin-Amiot, ?cole des Mines de Nantes

Pierre Cointe, ?cole des Mines de Nantes

Yann-Gaël Guéhéneuc, ?cole des Mines de Nantes

Narendra Jussien, ?cole des Mines de Nantes

pp. 166

PDF

Connectors Synthesis for Deadlock-Free Component-Based Architectures (Abstract)

Paola Inverardi, Universit? dell?Aquila

Simone Scriboni, Universit? dell?Aquila

pp. 174

PDF

Session IV-A: Analysis/Real Time

Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ (Abstract)

Kazuhiro Ogata, JAIST

Kokichi Futatsugi, JAIST

pp. 185

PDF

Generation of Distributed System Test-Beds from High-Level Software Architecture Descriptions (Abstract)

John Grundy, University of Auckland

Yuhong Cai, University of Auckland

Anna Liu, CSIRO Mathematical and Information Sciences

pp. 193

PDF

Tailoring a COTS Group Support System for Software Requirements Inspection (Abstract)

Michael Hallin, Vienna University of Technology

Paul Grünbacher, Johannes Kepler University Linz

Stefan Biffl, Fraunhofer Institute for Experimental Software Engineering

pp. 201

PDF

Session IV-B: Reverse Engineering and Integration

Automatically Restructuring Programs for the Web (Abstract)

Paul Graunke, Northeastern University

Robert Bruce Findler, Rice Univeristy

Shriram Krishnamurthi, Brown University

Matthias Felleisen, Northeastern University

pp. 211

PDF

Unfriendly COTS Integration-Instrumentation and Interfaces for Improved Plugability (Abstract)

Alexander Egyed, Teknowledge Corporation

Robert Balzer, Teknowledge Corporation

pp. 223

PDF

Adequate Reverse Engineering (Abstract)

Spencer Rugaber, Georgia Institute of Technology

Terry Shikano, Georgia Institute of Technology

R. E. Kurt Stirewalt, Michigan State University

pp. 232

PDF

Session V-A: Model Checking

Enhancing Partial-Order Reduction via Process Clustering (Abstract)

Twan Basten, Eindhoven University of Technology

Dragan Bosnacki, Eindhoven University of Technology

pp. 245

PDF

Exploiting Heap Symmetries in Explicit-State Model Checking of Software (Abstract)

Radu Iosif, Kansas State University

pp. 254

PDF

Combining Static Analysis and Model Checking for Software Analysis (Abstract)

Guillaume Brat, Kestrel/NASA Ames Research Center

Willem Visser, RIACS/NASA Ames Research Center

pp. 262

PDF

Session V-B: Specification and Model Engineering

Towards a Precise Definition of the OMG/MDA Framework (Abstract)

Jean Bézivin, Universit? de Nantes

Olivier Gerbé, HEC - Montr?al

pp. 273

PDF

Shared Variables Interaction Diagrams (Abstract)

Rajeev Alur, University of Pennsylvania

Radu Grosu, State University of New York at Stony Brook

pp. 281

PDF

Modeling Class Operations in B: Application to UML Behavioral Diagrams (Abstract)

Hung LEDANG, LORIA - Universit? Nancy 2

Jeanine SOUQUIÈRES, LORIA - Universit? Nancy 2

pp. 289

PDF

Automated Software Engineering Using Concurrent Class Machines (Abstract)

Radu Grosu, State University of New York at Stony Brook

Yanhong A. Liu, State University of New York at Stony Brook

Scott Smolka, State University of New York at Stony Brook

Scott D. Stoller, State University of New York at Stony Brook

Jingyu Yan, State University of New York at Stony Brook

pp. 297

PDF

Short Papers

Higher Order Function Synthesis Through Proof Planning (Abstract)

Andrew Cook, Heriot-Watt University

Andrew Ireland, Heriot-Watt University

Greg Michaelson, Heriot-Watt University

pp. 307

PDF

AGATE, Access Graph-Based Tools for Handling Encapsulation (Abstract)

G. Ardourel, LIRMM

M. Huchard, LIRMM

pp. 311

PDF

A UML Validation Toolset Based on Abstract State Machines (Abstract)

Wuwei Shen, The University of Michigan

Kevin Compton, The University of Michigan

James Huggins, Kettering University

pp. 315

PDF

Semi-Automated Verification of Erlang Code (Abstract)

Lars-Åke Fredlund, Swedish Institute of Computer Science

Dilian Gurov, Swedish Institute of Computer Science

Thomas Noll, Aachen University of Technology

pp. 319

PDF

Automatic Verification of Java Design Patterns (Abstract)

Alex Blewitt, University of Edinburgh

Alan Bundy, University of Edinburgh

Ian Stark, University of Edinburgh

pp. 324

PDF

Tracing Execution of Software for Design Coverage (Abstract)

Raimondas Lencevicius, Nokia Research Center

Edu Metz, Nokia Research Center

Alexander Ran, Nokia Research Center

pp. 328

PDF

Model Checking for an Executable Subset of UML (Abstract)

Fei Xie, University of Texas at Austin

Vladimir Levin, Bell Laboratories

James C. Browne, University of Texas at Austin

pp. 333

PDF

A Technique for Mutation of Java Objects (Abstract)

James M. Bieman, Colorado State University

Sudipto Ghosh, Colorado State University

Roger T. Alexander, Colorado State University

pp. 337

PDF

Providing Early Feedback in the Development Cycle Through Automated Application of Model Checking to Software Architectures (Abstract)

K. Suzanne Barber, University of Texas at Austin

Thomas Graser, University of Texas at Austin

Jim Holt, Motorola

pp. 341

PDF

Automated Check of Architectural Models Consistency Using SPIN (Abstract)

Paola Inverardi, Universit? dell?Aquila - Via Vetoio

Henry Muccini, Universit? dell?Aquila - Via Vetoio

Patrizio Pelliccione, Universit? dell?Aquila - Via Vetoio

pp. 346

PDF

Automating the Performance and Reliability Analysis of Enterprise Information Systems (Abstract)

Apostolos Zarras, INRIA Rocquencourt

Valerie Issarny, INRIA Rocquencourt

pp. 350

PDF

An Analysis-Revision Cycle to Evolve Requirements Specifications (Abstract)

A. S. d?Avila Garcez, Imperial College

A. Russo, Imperial College

B. Nuseibeh, The Open University

J. Kramer, Imperial College

pp. 354

PDF

Knowledge Base Approach to Consistency Management of UML Specifications (Abstract)

Andrea Zisman, City University

Alexander Kozlenkov, City University

pp. 359

PDF

Strategies for Automated Specification-Based Testing of Synchronous Software (Abstract)

Ioannis Parissis, LSR-IMAG

Jérôme Vassy, LSR-IMAG

pp. 364

PDF

Developing Generative Frameworks Using XML (Abstract)

Iain McLaren, Searchspace Limited

Tony Wicks, Searchspace Limited

pp. 368

PDF

A Tool for Lazy Verification of Security Protocols (Abstract)

Y. Chevalier, LORIA - UHP - UN2

L. Vigneron, LORIA - UHP - UN2

pp. 373

PDF

Generation of Functional Test Sequences from B Formal Specifications-Presentation and Industrial Case Study (Abstract)

Bruno Legeard, Laboratoire d?Informatique de l?Universit? de Franche-Comt?

Fabien Peureux, Laboratoire d?Informatique de l?Universit? de Franche-Comt?

pp. 377

PDF

Action Language Verifier (Abstract)

Tevfik Bultan, University of California

Tuba Yavuz-Kahveci, University of California

pp. 382

PDF

Scalable Consistency Checking Between Diagrams-The ViewIntegra Approach (Abstract)

Alexander Egyed, Teknowledge Corporation

pp. 387

PDF

Better Reasoning About Software Engineering Activities (Abstract)

Tim Menzies, University of British Comlumbia

James D. Kiper, Miami University

pp. 391

PDF

Amphion/NAV: Deductive Synthesis of State Estimation Software (Abstract)

Jon Whittle, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Jeffrey Van Baalen, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Johann Schumann, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Peter Robinson, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Tom Pressburger, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

John Penix, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Phil Oh, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Michael Lowry, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

Guillaume Brat, NASA, QSS, RIACS, Kestrel Tech., U. Wyoming, NASA Ames Research Center

pp. 395

PDF

Programs Are Abstract Data Types (Abstract)

Martin Erwig, Oregon State University

pp. 400

PDF

An Automated Tool for Analyzing Petri Nets Using SPIN (Abstract)

Gerald C. Gannod, Arizona State University

Sunil Gupta, Arizona State University

pp. 404

PDF

Formally Testing Fail-Safety of Electronic Purse Protocols (Abstract)

Jan Jürjens, University of Oxford

Guido Wimmel, Technische Universit?t M?nchen

pp. 408

PDF

Automata-Based Verification of Temporal Properties on Running Programs (Abstract)

Dimitra Giannakopoulou, NASA Ames Research Center

Klaus Havelund, NASA Ames Research Center

pp. 412

PDF

Towards an Evolutionary Formal Software Development (Abstract)

Dieter Hutter, German Research Center for Artificial Intelligence

Axel Schairer, German Research Center for Artificial Intelligence

pp. 417

PDF

A Concurrency Test Tool for Java Monitors (Abstract)

Brad Long, The University of Queensland, Brisbane

Dan Hoffman, University of Victoria

Paul Strooper, The University of Queensland, Brisbane

pp. 421

PDF

Enforcing Business Policies Through Automated Reconfiguration (Abstract)

L. Andrade, ATX Software SA

J.L. Fiadeiro, ATX Software SA; Univ. Lisbon

M. Wermelinger, ATX Software SA; Univ. Lisbon

pp. 426

PDF

Doctoral Symposium Abstracts

Design Rationale for Software Maintenance (PDF)

Janet E. Burge, Worcester Polytechnic Institute

David C. Brown, Worcester Polytechnic Institute

pp. 433

Security Specification and Verification (PDF)

Pascal Fenkam, Technical University of Vienna, Austria

pp. 434

Implementation of Specification Conjunction and Domain Interaction in Rosetta (PDF)

Cindy Kong, University of Kansas, USA

pp. 435

Automatic Translation from UML Specifications to B (PDF)

Hung LeDang, University of Nancy 2, France

pp. 436

Automated Conversion from a Requirements Document to an Executable Formal Specification (PDF)

Beum-Seuk Lee, University of Alabama at Birmingham

pp. 437

Automated Test-Data Generation from Formal Models of Software (PDF)

Sanjai Rayadurgam, University of Minnesota, USA

pp. 438

Model-Checking Real-Time Concurrent Systems (PDF)

Ilya Romanovsky, University of Durham, UK

pp. 439

Verify Properties of Mobile Code (PDF)

Songtao Xia, (Oregon Health Science University, USA)

pp. 440

Author Index (PDF)

pp. 441