ISoLA 2006: Paphos, Cyprus

Invited Talks

• John S. Fitzgerald, Peter Gorm Larsen:
  Triumphs and Challenges for Model-Oriented Formal Methods: The VDM⁺⁺ Experience (Abstract). 1-4
  
• David von Oheimb:
  Formal Security Analysis in Industry, at the Example of Electronic Distribution of Aircraft Software (EDS). 5
  
• Thomas Jensen:
  Certificates of Resource Usage on Mobile Telephones. 6-7
  
• Joseph Kiniry:
  Program Safety via Programmer Safety. 8
  
• Kai Richter:
  The AUTOSAR Timing Model - Status and Challenges -. 9-10
  
• Wolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, Kathrin Kaschner:
  Analysis Techniques for Service Models. 11-17
  

Keynote

• Michael G. Hinchey, Thomas Pressburger, Martin S. Feather, Lawrence Markosian, Wes Deadrick:
  Software Assurance Research Infusion: The NASA Experience. 18-27
  

Track on Formal Methods in Avionics and Aerospace Applications

• Mohammed Al Achhab, Ahmed Hammad, Hassan Mountassir:
  Verifying LTL Properties on Hierarchical Systems: Application to Aircraft Autopilot. 28-35
  
• Yamine Aït Ameur, Remi Delmas, Alexandre Cortier, Virginie Wiels:
  Formal Modelling of Avionics Systems. An Approach Based on Category Theory and the EXPRESS Modelling Language. 36-44
  
• David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
  Reasoning about Airport Security Regulations Using the Focal Environment. 45-52
  

Track on Formal Specifications in Practice

• Vadim Mutilin:
  Concurrent Testing of Java Components Using Java PathFinder. 53-59
  
• Alexander Kamkin:
  The UniTESK Approach to Specification-Based Validation of Hardware Designs. 60-66
  
• Laura Kovács, Nikolaj Popov, Tudor Jebelean:
  Combining Logic and Algebraic Techniques for Program Verification in Theorema. 67-74
  
• Sergey V. Zelenov, Denis V. Silakov, Alexander K. Petrenko, Mirko Conrad, Ines Fey:
  Automatic Test Generation for Model-Based Code Generators. 75-81
  
• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney:
  Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties. 82-90
  
• Jeremy Bryans, John S. Fitzgerald, Cliff B. Jones, Igor Mozolevsky:
  Formal Modelling of Dynamic Coalitions, with an Application in Chemical Engineering. 91-98
  

Poster Session

• Sébastien Labbé, Arnault Lapitre:
  CARVER: A Slicing Tool for Communicating Automata Specifications. 99-102
  
• Christian Buckl, Alois Knoll, Gerhard Schrott:
  Model-Based Development of Fault-Tolerant Embedded Software. 103-110
  
• Leif Pedersen, Hassan Reza:
  A Formal Specification of a Programming Language: Design of Pit. 111-118
  

Track on Safety and Security

• Christian Hammer, Jens Krinke, Frank Nodes:
  Intransitive Noninterference in Dependence Graphs. 119-128
  
• June Andronick:
  Formally Proved Anti-tearing Properties of Embedded C Code. 129-136
  
• Xianghua Deng, Robby, John Hatcliff:
  Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. 137
  
• Ewen Denney, Bernd Fischer:
  Extending Source Code Generators for Evidence-Based Software Certification. 138-145
  

Track on Evolutionary Computing Applied to Engineering

• Sabah Khalid, Mohsin Khan, Ping Wang, Xiaohui Liu, Suling Li:
  Application of Bioinformatics in the Design of Gene Expression Microarrays. 146-160
  
• M. Saud, I. I. Esat:
  A Novel Method for Obtaining Real Time Control Strategy Using GA for Dynamical Systems Subjected to External Arbitrary Excitations. 161-168
  
• F. S. Alfares, I. I. Esat:
  Real-Coded Quantum Inspired Evolution Algorithm Applied to Engineering Optimization Problems. 169-176
  

Track on Organic Computing

• Matthias Güdemann, Frank Ortmeier, Wolfgang Reif:
  Safety and Dependability Analysis of Self-Adaptive Systems. 177-184
  
• Jürgen Branke, Moez Mnif, Christian Müller-Schloer, Holger Prothmann, Urban Richter, Fabian Rochner, Hartmut Schmeck:
  Organic Computing - Addressing Complexity by Controlled Self-Organization. 185-191
  
• Steffen Stein, Arne Hamann, Rolf Ernst:
  Real-Time Property Verification in Organic Computing Systems. 192-197
  
• Sándor P. Fekete, Christiane Schmidt, Axel Wegener, Stefan Fischer:
  Recognizing Traffic Jams with Hovering Data Clouds. 198-203
  

Track on Timing Analysis in the Industrial Development Process

• Jan Staschulat, Jörn-Christian Braam, Rolf Ernst, Thomas Rambow, Rainer Schlör, Rainer Busch:
  Cost-Efficient Worst-Case Execution Time Analysis in Industrial Practice. 204-211
  
• Daniel Sehlberg, Andreas Ermedahl, Jan Gustafsson, Björn Lisper, Steffen Wiegratz:
  Static WCET Analysis of Real-Time Task-Oriented Code in Vehicle Control Systems. 212-219
  
• Christian Ferdinand, Reinhold Heckmann, Hans-Jörg Wolff, Christian Renz, Manabendra Gupta, Oleg Parshin:
  Towards an Integration of Low-Level Timing Analysis and Model-Based Code Generation. 220-226
  
• Pascal Montag, Steffen Görzig, Paul Levi:
  Challenges of Timing Verification Tools in the Automotive Domain. 227-232
  
• Jan Gustafsson:
  The Worst Case Execution Time Tool Challenge 2006. 233-240
  
• Lili Tan:
  The Worst Case Execution Time Tool Challenge 2006: The External Test. 241-248
  

Track on Formal Approaches to the Specification and Verification of Sensor Networks

• Michele Garetto, Marco Gribaudo:
  Model Checking Techniques for the Performance Analysis of Delay Tolerant Networks with On-off Behavior. 249-254
  
• Paolo Ballarini, Alice Miller:
  Model Checking Medium Access Control for Sensor Networks. 255-262
  
• A. K. McIver, Ansgar Fehnker:
  Formal Techniques for the Analysis of Wireless Networks. 263-270
  
• Akim Demaille, Sylvain Peyronnet, Benoît Sigoure:
  Modeling of Sensor Networks Using XRM. 271-276
  
• T. E. Daniel, S. N. I. Mount, Robert M. Newman, Elena I. Gaura:
  "Towards a Trusted Compiler for a Query Language for Wireless Sensor Networks.". 277-282
  
• Rachel Cardell-Oliver, Mark Reynolds, Mark Kranz:
  A Space and Time Requirements Logic for Sensor Networks. 283-289
  
• Matthias Fruth:
  Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol. 290-297
  

Track on Biologically-Inspired Computing

• Carolyn L. Talcott:
  Formal Executable Models of Cell Signaling Primitives. 298-302
  
• Christian Kubczak, Tiziana Margaria, Arno Fritsch, Bernhard Steffen:
  Biological LC/MS Preprocessing and Analysis with jABC, jETI and xcms. 303-308
  

Track on Applications of Rigorous and Formal Methods to Service-Oriented Computing

• Sidney Rosario, Albert Benveniste, Stefan Haar, Claude Jard:
  Foundations for Web Services Orchestrations: Functional and QoS Aspects, Jointly. 309-316
  
• Markus Bajohr, Tiziana Margaria, Bernhard Steffen:
  Service Based Enabling Service Availability in the MaTRICS: A Model-Driven Approach. 317-324
  
• Reinhold Kröger, Ulrike Lucke, Markus Schmid, Djamshid Tavangarian:
  Web Services for the Integration of XML-Based Content into Learning Platforms: A Three-level Model. 325-331
  
• Abílio Fernandes, Karin Koogan Breitman, Tatiana Almeida S. C. Vieira, Marco A. Casanova, Antonio L. Furtado:
  Semi-automated Workflow Synthesis. 332-334
  

Track on Highly Reliable Software: Theories, Methods, Tools and Experiences in China and South Africa

• Jin Song Dong, Yuzhang Feng, Jing Sun, Jun Sun:
  Context Awareness Systems Design and Reasoning. 335-340
  
• Farn Wang:
  REDLIB for the Formal Verification of Embedded Systems. 341-346
  
• Ankit Goel, Abhik Roychoudhury:
  Synthesis and Traceability of Scenario-Based Executable Models. 347-354
  
• Ji Wang, Xiaodong Yi, Xuejun Yang:
  Towards a Framework for Scalable Model Checking of Concurrent C Programs. 355-362
  
• Geguang Pu, Huibiao Zhu, Jifeng He, Zongyan Qiu, Hongli Yang, Xiangpeng Zhao:
  Patterns with Algebraic Properties in BPEL0. 363-370
  
• Zhiming Liu, Vladimir Mencl, Anders P. Ravn, Lu Yang:
  Harnessing Theories for Tool Support. 371-382
  
• Naijun Zhan:
  Connecting Algebraic and Logical Descriptions of Concurrent Systems. 383-391
  
• Jianhua Zhao, Bin Lei, Xuandong Li, Guoliang Zheng:
  Improve Model Checking Efficiency Using Specific Knowledge about the System. 392-396
  

Thematic Session on FMICS: Formal Methods for Industrial Critical Systems

• José M. Alvarez, Pedro de la Cámara, Jesús Martínez, Pedro Merino, Francisco C. Perez, Victoria Morillo:
  An SDL Implementation of the UMTS Radio Resource Control Protocol Oriented to Conformance Testing. 397-401
  
• Tiziana Margaria, Christian Kubczak, Bernhard Steffen, Stefan Naujokat:
  The FMICS-jETI Platform: Status and Perspectives. 402-407
  

Thematic Session on Validation and Verification in the Large

• Peter T. Breuer, Simon Pickin:
  Verification in the Large via Symbolic Approximation. 408-415
  
• María-del-Mar Gallardo, Christophe Joubert, Pedro Merino:
  Implementing Influence Analysis Using Parameterised Boolean Equation Systems. 416-424
  
• Dubravka Ilic, Elena Troubitsyna, Linas Laibinis, Sari Leppänen:
  Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication Protocols. 425-432
  
• Christian Wagner, Tiziana Margaria, Hans-Georg Pagendarm:
  Comparative Analysis of Tools for Automated Software Re-engineering Purposes. 433-440
  

Session on System Modelling and Verification

• Jürgen Großmann, Wolfgang Müller:
  A Formal Behavioral Semantics for TestML. 441-448
  
• Sarfraz Khurshid, Muhammad Zubair Malik, Engin Uzuncaova:
  An Automated Approach for Writing Alloy Specifications Using Instances. 449-457
  
• Yosi Ben-Asher, Eitan Farchi, Yaniv Eytani, Shmuel Ur:
  Noise Makers Need to Know Where to be Silent - Producing Schedules That Find Bugs. 458-465
  
• Bastian Schlich, Stefan Kowalewski:
  [mc]square: A Model Checker for Microcontroller Code. 466-473