ISoLA 2004: Paphos, Cyprus - Preliminary proceedings

Tiziana Margaria, Bernhard Steffen, Anna Philippou, Manfred Reitenspieß (Eds.): International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004, October 30 - November 2, 2004, Paphos, Cyprus. Preliminary proceedings. Technical Report TR-2004-6 Department of Computer Science, University of Cyprus 2004

Thematic session: Program Analysis and Transformation

Daniel J. Quinlan, Markus Schordan, Qing Yi, Andreas Sæbjørnsen: Classification and Utilization of Abstractions for Optimization. 2-9
Wolf Zimmermann: On the Correctness of Transformations in Compiler Back-Ends. 10-17
Byron Cook: Finding API usage rule violations in Windows device drivers using Static Driver Verifier. 18-18

Thematic session: From Processes via Workflows to Services

Jörg Becker: Project Management for Process Management - a Procedural Model for Process-Oriented Reorganisation Projects. 19-27
Jens Hündling, Mathias Weske: Modeling Quality of Services in Service Oriented Environments. 28-34
Kirsten Lenz, Andreas Oberweis: Workflow Services: A Petri Net-Based Approach to Web Services. 35-41
Rey Abe, Martin Beinhart, Stefan Biffl, eva Kühn, Markus Ly, Bettina Thurnher: Need for Rigorous Methods and Tools in Collaborative Mobile Software Solutions - a Use Case Study on a "Travel Service Application". 42-44

Thematic session: Structured Data Tools

Pieter J. Toussaint, Leo Wolf: The Narrator System: processing, storing and retrieving medical, narrative data. 45-50
Joost Jacob: A Rule Markup Language and its application to UML. 51-57
Dave Clarke, David Costa, Farhad Arbab: Modelling Coordination in Biological Systems. 58-66
Joost Jacob, Frank S. de Boer, Marcello M. Bonsangue, Andries Stam, Leendert van der Torre: Using XML Transformations for Enterprise Architectures. 67-73

Regular papers: Model Checking and Validation

Yamine Aït Ameur, Mickaël Baron: Bridging the gap between formal and experimental validation approaches in HCI systems design: use of the event B proof based technique. 74-80
María Alpuente, Demis Ballis, Moreno Falaschi: Automated Verification of Web Sites Using Partial Rewriting. 81-88
Shady Copty, Shai Fine, Shmuel Ur, Avi Ziv: Probabilistic Alternative Regression Suites. 89-91
Tudor Jebelean, Laura Kovács, Nikolaj Popov: Experimental Program Verification in the Theorema System. 92-99

Regular papers: Formal Methods in Industry

Christopher A. Rouff, Amy Vanderbilt, Walter Truszkowski, James L. Rash, Michael G. Hinchey: Formal Methods for Autonomic and Swarm-based Systems. 100-102
Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue Simonsen, Christian Stefansen: Compositional Specification of Commercial Contracts. 103-110

Thematic session: Error Analysis and Model-based Testing Tools

Parosh Aziz Abdulla, Johan Deneaux, Gunnar Stålmarck, Herman Ågren, Ove Åkerlund: Designing Safe, Reliable Systems using Scade. 111-118
Johan Andersson, Christer Norström, Anders Wall: Decreasing Maintenance Costs by Introducing Formal Models and Analysis of Real-Time Systems in Industrial Settings. 119-125
Andreas Ermedahl, Jan Gustafsson, Björn Lisper, Daniel Sandell: Static Timing Analysis of Real-Time Operating Systems Code. 126-133

Panel: Formal Approaches to Complex Software Systems

Regular papers: Software Technology

Doral Lucanu: A Logical Foundation of the OWL Languages. 135-142
Gabriel Alves, Adilson Arcoverde, Ricardo Massa Ferreira Lima, Paulo Romero Martins Maciel: EZPetri: A Petri net interchange framework for Eclipse based on PNML. 143-149
eva Kühn, Fabian Schmied: Distributed Peer-to-Peer Application development with Declarative and Aspect-Oriented techniques. 150-156

Regular papers: Model Checking and Validation

Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang: Efficient SAT-based Bounded Model Checking for Software Verification. 157-164
Radu Grosu, Scott A. Smolka: Quantitative Model checking. 165-174
Shoham Ben-David, Dana Fisman, Sitvanit Ruah: Embedding Finite Automata within regular Expressions. 175-180
Martin Freibothe, Jens Schönherr, Bernd Straube, Jörg Bormann: Semi-formal Verification of the quasi-static behavior of Mixed-Signal Circuits by SAT-based Property Checking. 181-187

Thematic session: Industrial use of tools for formal analysis

Mirko Conrad: Formal Techniques for Analysing and Testing Automotive Control Software developed in a Model-based Way. 188-188
Limor Fix: Abstract for the ISOLA Special Session on "Industrial use of tools for Formal Analysis". 189-189
Yaron Wolfsthal: Abstract for the ISOLA Special Session on "Industrial use of tools for Formal Analysis". 190-190
Jianli Xu: Application of formal methods in Nokia mobile terminal and network software system development. 190-190

Thematic session: Dependable component-based and networked applications

Henrik Eichenhardt, Elke Franz, Simone Röttger, Ute Wappler: Adapting Component Models to Support Responsibility. 191-193
Ramesh Rharadwaj: Development of Dependable Component-Based Distributed Applications. 194-200

Thematic session: Scheduling and Performance of Real-time Embedded Systems

Martijn Hendriks, Barend van den Nieuwelaar, Frits W. Vaandrager: Model Checker Aided Design of a Controller for a Wafer Scanner. 201-208
Marcel Verhoef, Ernesto Wandeler, Lothar Thiele, Paul Lieverse: System Architecture Evaluation Using Modular Performance Analysis - A Case Study. 209-219
Oana Florescu, Jeroen Voeten, Henk Corporaal: A Unified Model for Analysis of Real-Time Properties. 220-226

Thematic session: Parametrised model-checking

Muffy Calder, Alice Miller: Verifying parametrized, featured networks by abstraction. 227-234
Michael Huth, Altaf Hussain: On model checking multiple hybrid views. 235-242
Saddek Bensalem, Doron Peled, Hongyang Qu, Stavros Tripakis: Automatic Generation of Path Conditions for Timed Systems. 243-249

Thematic session: Analysis and Verification of Component-Based Systems

Harini Srinivasan, Darrell Reimer, Aaron Kershenbaum, Edith Schonberg, Kavitha Srinivas: Static validation of resource management in large Java applications. 250-252
Jakob Rehof, Sriram K. Rajamani: Models for Contract Conformance. 253-260
Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer: A Case Study in Domain-customized Model Checking for Real-time Component Software. 261-267

Thematic session: Formal Methods for Quantitative Analysis of Systems

Marie Duflot, Marta Z. Kwiatkowska, Gethin Norman, David Parker: A Formal Analysis of Bluetooth Device Discovery. 268-275
Simona Bernardi, Susanna Donatelli, Giovanna Dondossola: A class Diagram framework for collecting dependability requirements in automation systems. 276-283
Henrik C. Bohnenkamp, Holger Hermanns, David N. Jansen, Joost-Pieter Katoen, Yaroslav S. Usenko: An industrial-strength formal method -- A Modest survey. 284-295

Regular papers: Case Studies

Erwan Jahier, Pascal Raymond, Philippe Baufreton: Case Studies with Lurette V2. 296-303
Søren Christensen, Jens Bæk Jørgensen, Antti-Pekka Tuovinen, Jianli Xu: Estimation of Memory Usage of Mobile Phone Software Using UML and Coloured Petri Nets. 304-310

Thematic session: Model Based Testing og Large-scale and Real-Time Systems

Victor V. Kuliamin: Model Based Testing of Large-scale Software: How Can Simple Models Help to Test Complex System. 311-316
Daniel Mika, Josef Strnadel, Kotásek Zdenik: The Identification of registers in RTL Structures for the Test Application. 317-319

Thematic session: Formal Methods for Quantitative Analysis of Systems

Joern Ploennigs, Mario Neugebauer, Klaus Kabitzsch: Automated Model Generation from Design Databases at the Example of Building Automation Networks. 320-327
Peter Buchholz, Falko Bause, Carsten Tepper: The ProC/B-Approach from informal descriptions to formal models. 328-334

Thematic session: Adaption of Formal Methods for Industry

Francois Carcenac, Frédéric Boniol: Verification of an avionic system using timed model checking. 335-342
Dmitrij Koznov, Maxim Katrashov, Goman Gagarsky, Vera A. Zvereva, Alexey Barsov: Round-trip engineering of reactive systems. 343-347