The Community for Technology Leaders
Engineering of Complex Computer Systems, IEEE International Conference on (2007)
Auckland, New Zealand
July 11, 2007 to July 14, 2007
ISBN: 0-7695-2895-3
TABLE OF CONTENTS

POSIX file store in Z/Eves: an experiment in the verified software repository (Abstract)

Leo Freitas , University of York, UK
Zheng Fu , University of York, UK
Jim Woodcock , University of York, UK
pp. 3-14
Introduction

Preface (PDF)

pp. xi
Keynote Speaker

POSIX file store in Z/Eves: an experiment in the verified software repository (Abstract)

Leo Freitas , University of York, UK
Zheng Fu , University of York, UK
Jim Woodcock , University of York, UK
pp. 3-14
Real-time Systems

Just-in-Time Certification (Abstract)

John Rushby , SRI International, USA
pp. 15-24

Modular Synthesis of Discrete Controllers (Abstract)

Petra Malik , University of Waikato, New Zealand
Robi Malik , University of Waikato, New Zealand
David Streader , University of Waikato, New Zealand
Steve Reeves , University of Waikato, New Zealand
pp. 25-34
Modeling and Verification

Model Checking-based Verification of Web Application (Abstract)

Huaikou Miao , Shanghai University, China
Hongwei Zeng , Shanghai University, China; Wuhan University, China
pp. 47-55

A light-weight static approach to analyzing UML behavioral properties (Abstract)

Lijun Yu , Colorado State University, USA
Robert B. France , Colorado State University, USA
Indrakshi Ray , Colorado State University, USA
Kevin Lano , Kings College, UK
pp. 56-63

A Formal Model for Compensable Transactions (Abstract)

Jing Li , East China Normal University, China
Huibiao Zhu , East China Normal University, China
Geguang Pu , East China Normal University, China
Jifeng He , East China Normal University, China
pp. 64-73

A Formal Semantic Model of the Semantic Web Service Ontology (WSMO) (Abstract)

Hai H. Wang , University of Southampton, UK
Nick Gibbins , University of Southampton, UK
Terry Payne , University of Southampton, UK
Ahmed Saleh , University of Southampton, UK
Jun Sun , National University of Singapore, Singapore
pp. 74-86
Keynote Speaker

Selecting V&V Technology Combinations: How to Pick a Winner? (Abstract)

Paul Strooper , The University of Queensland, Australia
Margaret A. Wojcicki , The University of Queensland, Australia
pp. 87-96
Safety and Security

A Novel Approach to the Detection of Cheating in Multiplayer Online Games (Abstract)

Peter Laurens , University of York, UK
Richard F. Paige , University of York, UK
Phillip J. Brooke , University of Teesside, UK
Howard Chivers , Cranfield University, UK
pp. 97-106

Reasoning about Nonblocking Concurrency using Reduction (Abstract)

Lindsay Groves , Victoria University of Wellington, New Zealand
pp. 107-116

A Combined Approach for Information Flow Analysis in Fault Tolerant Hardware (Abstract)

Tim McComb , University of Queensland, Australia
Luke Wildman , University of Queensland, Australia
pp. 117-128
Context Awareness and Ubiquitous Computing

The Registry for Sensor Network Discovery (Abstract)

Jeongkyu Park , Korea Aerospace University, Korea
Jiung Han , Korea Aerospace University, Korea
Kibong Kang , Korea Aerospace University, Korea
Keung Hae Lee , Korea Aerospace University, Korea
pp. 129-137

An agent based approach to examining shared situation awareness (Abstract)

Simon Connelly , University of Queensland, Australia
Peter Lindsay , University of Queensland, Australia
Marcus Gallagher , University of Queensland, Australia
pp. 138-147

Product Line Enabled Intelligent Mobile Middleware (Abstract)

Weishan Zhang , Tongji University, China
Thomas Kunz , Carleton University, Canada
Klaus Marius , Hansen University of Aarhus, Denmark
pp. 148-160
Keynote Speaker
Formal Languages

Belief-augmented OWL (BOWL) Engineering the SemanticWeb with Beliefs (Abstract)

Yuzhang Feng , National University of Singapore, Singapore
Yuan Fang Li , National University of Singapore, Singapore
Colin Keng-Yan Tan , National University of Singapore, Singapore
Bimlesh Wadhwa , National University of Singapore, Singapore
Hai Wang , University of Southampton, United Kingdom
pp. 165-174

A Formal Contract Language for Plugin-based Software Engineering (Abstract)

Jens Dietrich , Massey University, New Zealand
John Hosking , University of Auckland, New Zealand
Jonathan Giles , Massey University, New Zealand
pp. 175-184

Linking Object-Z with Spec# (Abstract)

Shengchao Qin , Durham University, UK
Guanhua He , Durham University, UK
pp. 185-196
Software Architecture

Communicating Software Architecture using a Unified Single-View Visualization (Abstract)

Thomas Panas , Lawrence Livermore National Laboratory
Thomas Epperly , Lawrence Livermore National Laboratory
Daniel Quinlan , Lawrence Livermore National Laboratory
Andreas Saebjornsen , Lawrence Livermore National Laboratory
Richard Vuduc , Lawrence Livermore National Laboratory
pp. 217-228
Special Session: Addressing Complexity with Autonomic Systems

A first approach to the closed-form specification and analysis of an autonomic control system (Abstract)

Simon Dobson , UCD Dublin, Ireland
Eoin Bailey , UCD Dublin, Ireland
Stephen Knox , UCD Dublin, Ireland
Ross Shannon , UCD Dublin, Ireland
Aaron Quigley , UCD Dublin, Ireland
pp. 229-237

The Imminent Complexity Quagmire in Pervasive Computing--Autonomic Agents a Solution? (Abstract)

Roy Sterritt , University of Ulster, Northern Ireland
Sarah Eowyn , Johnston University of Ulster, Northern Ireland
Patricia O'Hagan , Core Systems, Belfast, Northern Ireland
Edward Hanna , Core Systems, Belfast, Northern Ireland
pp. 238-250
Special Session: Grand Challenges--Complex Program Verifier

Formalising Flash Memory: First Steps (Abstract)

Andrew Butterfield , Trinity College Dublin, Ireland
Jim Woodcock , University of York, UK
pp. 251-260

Formally Counting Electronic Votes (But Still Only Trusting Paper) (Abstract)

Joeseph Kiniry , University College Dublin, Ireland
pp. 261-269

What Use is Verified Software? (Abstract)

John Rushby , SRI International, USA
pp. 270-276

A Refinement Driven Component-Based Design (Abstract)

Zhenbang Chen , United Nations University
Zhiming Liu , United Nations University
Volker Stolz , United Nations University
Lu Yang , United Nations University
Anders P. Ravn , University of Aalborg, Denmark
pp. 277-289

Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository (Abstract)

Leo Freitas , University of York, UK
Konstantinos Mokos , University of York, UK
Jim Woodcock , University of York, UK
pp. 290-298

What Can the \pi-calculus Tell Us About the Mondex Purse System? (Abstract)

Cliff B. Jones , Newcastle University, UK
Ken G. Pierce , Newcastle University, UK
pp. 300-306

Automated Verification of Shape, Size and Bag Properties (Abstract)

Wei-Ngan Chin , National University of Singapore, Singapore; Singapore-MIT Alliance
Cristina David , National University of Singapore, Singapore
Huu Hai Nguyen , Singapore-MIT Alliance
Shengchao Qin , Durham University, UK
pp. 307-320
Special Session: Advances in the FMICS-jETI Platform for Program Verification

On-the-fly model checking for C programs with extended CADP in FMICS-jETI (Abstract)

María del Mar Gallardo , University of Malaga, Spain
Pedro Merino , University of Malaga, Spain
Christophe Joubert , Technical University of Valencia, Spain
David Sanán , University of Malaga, Spain
pp. 321-329

Parallel Model Checking and the FMICS-jETI Platform (Abstract)

Jirí Barnat , Masaryk University, Czech Republic
Lubos Brim , Masaryk University, Czech Republic
Martin Leucker , Technische Universitat Munchen, Germany
pp. 330-339

The LearnLib in FMICS-jETI (Abstract)

Tiziana Margaria , University of Potsdam, Germany
Harald Raffelt , University of Dortmund, Germany
Bernhard Steffen , University of Dortmund, Germany
Martin Leucker , TU Munchen, Germany
pp. 340-352
Selected Papers from the UML&AADL 2007 Workshop

Managing Complexity of Automotive Electronics Using the EAST-ADL (Abstract)

Philippe Cuenot , Siemens VDO, France
DeJiu Chen , Royal Institute of Technology, Sweden
Sébastien Gérard , CEA List, France
Henrik Lönn , Volvo Technology Corporation, Sweden
Mark-Oliver Reiser , Technical University of Berlin, Germany
David Servat , CEA List, France
Carl-Johan Sjöstedt , Royal Institute of Technology, Sweden
Ramin Tavakoli Kolagari , Technical University of Berlin, Germany
Martin Törngren , Royal Institute of Technology, Sweden
Matthias Weber , Carmeq GmbH, Germany
pp. 353-358

MARTE: Also an UML Profile for Modeling AADL Applications (Abstract)

Madeleine Faugère , Thales Research and Technology
Thimothée Bourbeau , Thales Research and Technology
Robert de Simone , INRIA, France
Sébastien Gérard , CEA LIST, France
pp. 359-364

From PIMs to PSMs (Abstract)

Peter H. Feiler , Carnegie Mellon University
Dio de Niz , Carnegie Mellon University
Chris Raistrick , Kennedy-Carter
Bruce A. Lewis , US Army, AMRDEC
pp. 365-370

The AADL behaviour annex -- experiments and roadmap (Abstract)

Ricardo Bedin França , IRIT-Universite Paul Sabatier, France
Jean-Paul Bodeveix , IRIT-Universite Paul Sabatier, France
Mamoun Filali , IRIT-Universite Paul Sabatier, France
Jean-François Rolland , IRIT-Universite Paul Sabatier, France
David Chemouil , Centre national d'etudes spatiales, Toulouse
Dave Thomas , EADS Astrium Satellites
pp. 377-382
Author Index

Author Index (PDF)

pp. 383
92 ms
(Ver 3.3 (11022016))