The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2004)
Beijing, China
Sept. 28, 2004 to Sept. 30, 2004
ISBN: 0-7695-2222-X
TABLE OF CONTENTS

Preface (PDF)

pp. 0_9

Preface (PDF)

pp. ix
Keynote 1

A Programming Model for the Orchestration of Web Services (Abstract)

Jayadev Misra , The University of Texas at Austin
pp. 2-11
Session 1A: Parallel Distributed Systems

Abstraction of Parallel Uniform Processes with Data (Abstract)

Jun Pang , CWI, The Netherlands
Jaco van de Pol , CWI, The Netherlands
Miguel Valero Espada , CWI, The Netherlands
pp. 14-23

Towards Mobile Processes in Unifying Theories (Abstract)

Xinbei Tang , University of Kent, UK
Jim Woodcock , University of Kent, UK
pp. 44-53
Session 1B: Automated Proof and Model Checking

Symbolic Verification of Infinite Systems using a Finite Union of DFAs (Abstract)

Suman Roy , Honeywell Technology Solutions Lab. Pvt. Ltd., India
pp. 56-66

Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems (Abstract)

Klaus Schneider , University of Kaiserslautern, Germany
Tobias Schuele , University of Kaiserslautern, Germany
pp. 67-76

Proof Reuse for Deductive Program Verification (Abstract)

Bernhard Beckert , University of Koblenz-Landau
Vladimir Klebanov , University of Koblenz-Landau
pp. 77-86
Keynote 2

Property-Driven Development (Abstract)

Martin Wirsing , Ludwig-Maximilians-Universit?t M?nchen, Germany
Hubert Baumeister , Ludwig-Maximilians-Universit?t M?nchen, Germany
Alexander Knapp , Ludwig-Maximilians-Universit?t M?nchen, Germany
pp. 96-102
Session 2A: System Modelling and Development

From Requirements Change to Design Change: A Formal Path (Abstract)

R. Geoff. Dromey , Griffith University, Australia
Lian. Wen , Griffith University, Australia
pp. 104-113

Decidability Results for Parametric Probabilistic Transition Systems with an Application to Security (Abstract)

Angelo Troina , Universit? di Pisa, Italy
Andrea Maggiolo-Schettini , Universit? di Pisa, Italy
Ruggero Lanotte , Universit? dell'Insubria, Italy
pp. 114-121

Towards Formalizing Behavioral Substitutability in Component Frameworks (Abstract)

Jean-Paul Rigault , Univ. of Nice Sophia Antipolis, France
Sabine Moisan , INRIA Sophia Antipolis, France
Annie Ressouche , INRIA Sophia Antipolis, France
pp. 122-131

Resource Models and Pre-Compiler Specification for Hardware/Software Co-Design Language (Abstract)

He Jifeng , United Nations University, Macau
Jin Naiyong , East China Normal University, China
pp. 132-141
Session 2B: Model Integration and Theory Unification

Modeling Peer-to-Peer Service Goals in UML (Abstract)

Richard Torbj? Sanders , SINTEF ICT / NTNU, Norway
Rolv Br? , Norwegian University of Science and Technology (NTNU), Norway
pp. 144-153

Past- and Future-Oriented Time-Bounded Temporal Properties with OCL (Abstract)

Stephan Flake , ORGA Systems GmbH, Germany
Wolfgang Mueller , Paderborn University / C-LAB, Germany
pp. 154-163

On Semantics and Refinement of UML Statecharts: A Coalgebraic View (Abstract)

Zhang Naixiao , Peking University
Sun Meng , Peking University
Lu?s S. Barbosa , Minho University
pp. 164-173

The Rhapsody UML Verification Environment (Abstract)

Ingo Schinz , OFFIS, Germany
Bernd Westphal , Carl von Ossietzky Universit?t Oldenburg, Germany
Tobe Toben , Carl von Ossietzky Universit?t Oldenburg, Germany
Christian Mrugalla , OFFIS, Germany
pp. 174-183
Keynote 3

Care, Feeding and Growth of Software Systems (PDF)

Mathai Joseph , Tata Research Development & Design Centre
pp. 186
Session 3: Object-Oriented and Component-Based Development

An Asynchronous Communication Model for Distributed Concurrent Objects (Abstract)

Einar Broch Johnsen , University of Oslo, Norway
Olaf Owe , University of Oslo, Norway
pp. 188-197

Models and Temporal Logics for Timed Component Connectors (Abstract)

Farhad Arbab , Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands; Universiteit Leiden, The Netherlands
Christel Baier , Universit?t Bonn, Germany
Jan Rutten , Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands; Vrije Universiteit Amsterdam, The Netherlands
Frank de Boer , Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands; Universiteit Leiden, The Netherlands
pp. 198-207

Glass-Box and Black-Box Views on Object-Oriented Specifications (Abstract)

Alexander Knapp , Ludwig-Maximilians-Universit?t M?nchen, Germany
Michel Bidoit , CNRS & ENS de Cachan, France
Rolf Hennicker , Ludwig-Maximilians-Universit?t M?nchen, Germany
Hubert Baumeister , Ludwig-Maximilians-Universit?t M?nchen, Germany
pp. 208-217

Exception Safety for C# (Abstract)

Wolfram Schulte , Microsoft Research, Redmond, WA
K. Rustan M. Leino , Microsoft Research, Redmond, WA
pp. 218-227
Keynote 4

Random Testing in Isabelle/HOL (Abstract)

Tobias Nipkow , Technische Universit?t M?nchen, Germany
Stefan Berghofer , Technische Universit?t M?nchen, Germany
pp. 230-239
Session 4A: Testing and Validation

Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques (Abstract)

Chen Xu , Chinese Academy of Sciences, China
Xiaoliang Wang , Chinese Academy of Sciences, China
Jian Zhang , Chinese Academy of Sciences, China
pp. 242-250

Test Case Generation Using Stochastic Automata Networks: Quantitative Analysis (Abstract)

Andr? G. Farina , Pontif?cia Universidade Cat?lica do Rio Grande do Sul, Brazil
Cristiano Bertolini , Pontif?cia Universidade Cat?lica do Rio Grande do Sul, Brazil
Fl?vio M. Oliveira , Pontif?cia Universidade Cat?lica do Rio Grande do Sul, Brazil
Paulo Fernandes , Pontif?cia Universidade Cat?lica do Rio Grande do Sul, Brazil
pp. 251-260

Generating Efficient Test Sets with a Model Checker (Abstract)

John Rushby , SRI International, Menlo Park, CA
Leonardo de Moura , SRI International, Menlo Park, CA
Gr?goire Hamon , Chalmers University of Technology, Sweden
pp. 261-270

Distributed Testing of Multi Input/Output Transition System (Abstract)

Xia Yin , Tsinghua University, China
Jianping Wu , Tsinghua University, China
Zhongjie Li , Tsinghua University, China
pp. 271-280

Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations (Abstract)

Benjamin Goldberg , New York University
Clark Barrett , New York University
Ying Hu , New York University
pp. 281-289
Session 4B: System Correctness Analysis and Refinement

Heuristics for Refinement Relations (Abstract)

J. W. Sanders , OUCL, UK
Florian Kamm? , Technische Universit?t Berlin, Germany
pp. 292-299

Towards Action Refinement for Concurrent Systems with Causal Ambiguity (Abstract)

Houguang Yue , Chinese Academy of Sciences, China
Jinzhao Wu , Universit?t Mannheim, Germany
pp. 300-309

Refine and Gabriel: Support for Refinement and Tactics (Abstract)

Marcel Oliveira , University of Kent, England
Ana Cavalcanti , University of Kent, England
Manuela Xavier , Universidade Federal de Pernambuco, Brazil
pp. 310-319

Automated Element-Wise Reasoning with Sets (Abstract)

Georg Struth , Universit? t Augsburg, Germany
pp. 320-329

A Formalism for Conformance Analysis and Its Applications (Abstract)

Ethan V. Munson , University of Wisconsin-Milwaukee
Tien N. Nguyen , University of Wisconsin-Milwaukee
pp. 330-339
Keynote 5

ABC: Supporting Software Architectures in the Whole Lifecycle (PDF)

Hong Mei , Peking University, Beijing, China
pp. 342-343
Session 5A: Architecture and Co-Design

Fault Tolerance in a Layered Architecture: A General Specification Pattern in B (Abstract)

Elena Troubitsyna , ?bo Akademi University, Finland
Linas Laibinis , ?bo Akademi University, Finland
pp. 346-355

Formal Derivation of Functional Architectural Design (Abstract)

Imen Bourguiba , McMaster University, Canada
Ridha Khedri , McMaster University, Canada
pp. 356-365

Verification of the WAP Transaction Layer (Abstract)

Ryszard Janicki , McMaster University, Canada
Yu-Tong He , McMaster University, Canada
pp. 366-375

An Approach to Hardware/Software Partitioning for Multiple Hardware Devices Model (Abstract)

Qiu Zongyan , Peking University, China
Pu Geguang , Peking University, China
Wang Shuling , Peking University, China
Zhao Xiangpeng , Peking University, China
Wang Yi , Uppsala University, Sweden
He Jifeng , United Nations University, Macau
pp. 376-385
Session 5B: Automated Analysis and Verification

The Formal, Tool Supported Development of Real Time Systems (Abstract)

Richard O. Sinnott , University of Glasgow, Scotland
pp. 388-395

Formal Verification of Requirements using SPIN: A Case Study on Web Services (Abstract)

Marco Pistore , DIT, University of Trento, Italy
Raman Kazhamiakin , DIT, University of Trento, Italy
Marco Roveri , ITC-irst, Italy
pp. 406-415

How to Verify Dynamic Properties of Information Systems (Abstract)

R?gine Laleau , Universit? Paris 12
Marc Frappier , Universit? de Sherbrooke, Canada
Helen Treharne , University of London
Neil Evans , University of London
pp. 416-425

Author Index (PDF)

pp. 427-428
94 ms
(Ver 3.3 (11022016))