12. ICECCS 2007: Auckland, New Zealand

Keynote Speaker

• Leo Freitas, Zheng Fu, Jim Woodcock:
  POSIX file store in Z/Eves: an experiment in the verified software repository. 3-14
  

Real-time Systems

• John M. Rushby:
  Just-in-Time Certification. 15-24
  
• Petra Malik, Robi Malik, David Streader, Steve Reeves:
  Modular Synthesis of Discrete Controllers. 25-34
  
• Anton Wijs:
  Achieving Discrete Relative Timing with Untimed Process Algebra. 35-46
  

Modeling and Verification

• Huaikou Miao, Hongwei Zeng:
  Model Checking-based Verification of Web Application. 47-55
  
• Lijun Yu, Robert B. France, Indrakshi Ray, Kevin Lano:
  A light-weight static approach to analyzing UML behavioral properties. 56-63
  
• Jing Li, Huibiao Zhu, Geguang Pu, Jifeng He:
  A Formal Model for Compensable Transactions. 64-73
  
• Hai H. Wang, Nick Gibbins, Terry R. Payne, Ahmed Saleh, Jun Sun:
  A Formal Semantic Model of the Semantic Web Service Ontology (WSMO). 74-86
  

Keynote Speaker

• Paul A. Strooper, Margaret A. Wojcicki:
  Selecting V&V Technology Combinations: How to Pick a Winner? 87-96
  

Safety and Security

• Peter Laurens, Richard F. Paige, Phillip J. Brooke, Howard Chivers:
  A Novel Approach to the Detection of Cheating in Multiplayer Online Games. 97-106
  
• Lindsay Groves:
  Reasoning about Nonblocking Concurrency using Reduction. 107-116
  
• Tim McComb, Luke Wildman:
  A Combined Approach for Information Flow Analysis in Fault Tolerant Hardware. 117-128
  

Context Awareness and Ubiquitous Computing

• Jeongkyu Park, Jiung Han, Kibong Kang, Keung Hae Lee:
  The Registry for Sensor Network Discovery. 129-137
  
• Simon Connelly, Peter A. Lindsay, Marcus Gallagher:
  An agent based approach to examining shared situation awareness. 138-147
  
• Weishan Zhang, Thomas Kunz, Klaus Marius Hansen:
  Product Line Enabled Intelligent Mobile Middleware. 148-160
  

Keynote Speaker

• Wolfram Schulte:
  Pex - An Intelligent Assistant for Rigorous Developer Testing. 161
  

Formal Languages

• Yuzhang Feng, Yuan-Fang Li, Colin Keng-Yan Tan, Bimlesh Wadhwa, Hai H. Wang:
  Belief-augmented OWL (BOWL) Engineering the SemanticWeb with Beliefs. 165-174
  
• Jens Dietrich, John G. Hosking, Jonathan Giles:
  A Formal Contract Language for Plugin-based Software Engineering. 175-184
  
• Shengchao Qin, Guanhua He:
  Linking Object-Z with Spec#. 185-196
  

Software Architecture

• Urjaswala Vora:
  Architectural Design Methodologies for Complex Evolving Systems. 197-206
  
• Tien Nguyen:
  EmVC: Managing Changes and Configurations in Designs of Complex, Embedded Computing Systems. 207-216
  
• Thomas Panas, Thomas Epperly, Daniel J. Quinlan, Andreas Sæbjørnsen, Richard W. Vuduc:
  Communicating Software Architecture using a Unified Single-View Visualization. 217-228
  

Addressing Complexity with Autonomic Systems

• Simon Dobson, Eoin Bailey, Stephen Knox, Ross Shannon, Aaron J. Quigley:
  A first approach to the closed-form specification and analysis of an autonomic control system. 229-237
  
• Roy Sterritt, Sarah Eowyn, Patricia O'Hagan, Edward Hanna:
  The Imminent Complexity Quagmire in Pervasive Computing - Autonomic Agents a Solution? 238-250
  

Grand Challenges - Complex Program Verifier

• Andrew Butterfield, Jim Woodcock:
  Formalising Flash Memory: First Steps. 251-260
  
• Joseph Kiniry:
  Formally Counting Electronic Votes (But Still Only Trusting Paper). 261-269
  
• John M. Rushby:
  What Use is Verified Software? 270-276
  
• Zhenbang Chen, Zhiming Liu, Volker Stolz, Lu Yang, Anders P. Ravn:
  A Refinement Driven Component-Based Design. 277-289
  
• Leo Freitas, Konstantinos Mokos, Jim Woodcock:
  Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. 290-298
  
• Wolfram Schulte:
  Experiments in Verifying Low Level Concurrent C Code. 299
  
• Cliff B. Jones, Ken G. Pierce:
  What Can the pi-calculus Tell Us About the Mondex Purse System? 300-306
  
• Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin:
  Automated Verification of Shape, Size and Bag Properties. 307-320
  

Advances in the FMICS-jETI Platform for Program Verification

• María-del-Mar Gallardo, Pedro Merino, Christophe Joubert, David Sanán:
  On-the-fly model checking for C programs with extended CADP in FMICS-jETI. 321-329
  
• Jiri Barnat, Lubos Brim, Martin Leucker:
  Parallel Model Checking and the FMICS-jETI Platform. 330-339
  
• Tiziana Margaria, Harald Raffelt, Bernhard Steffen, Martin Leucker:
  The LearnLib in FMICS-jETI. 340-352
  

Selected Papers from the UML&AADL 2007 Workshop

• Philippe Cuenot, De-Jiu Chen, Sébastien Gérard, Henrik Lönn, Mark-Oliver Reiser, David Servat, Carl-Johan Sjöstedt, Ramin Tavakoli Kolagari, Martin Törngren, Matthias Weber:
  Managing Complexity of Automotive Electronics Using the EAST-ADL. 353-358
  
• Madeleine Faugère, Thimothée Bourbeau, Robert de Simone, Sébastien Gérard:
  MARTE: Also an UML Profile for Modeling AADL Applications. 359-364
  
• Peter H. Feiler, Dionisio de Niz, Chris Raistrick, Bruce A. Lewis:
  From PIMs to PSMs. 365-370
  
• Isabelle Perseil, Laurent Pautet:
  A Co-Modeling Methodology Designed for RT Architecture Models Integration. 371-376
  
• Ricardo Bedin França, Jean-Paul Bodeveix, Mamoun Filali, Jean-François Rolland, David Chemouil, Dave Thomas:
  The AADL behaviour annex - experiments and roadmap. 377-382