Leveraging Applications of Formal Methods, Verification and Validation

1. Front Matter

   PDF

2. Invited Talks

   1. Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)

      • Manfred Broy

      Pages 1-13

   2. Information System Engineering Supporting Observation, Orientation, Decision, and Compliant Action

      • Dimitrios Georgakopoulos

      Pages 14-14

3. Keynote

   1. Modelling Coordination and Compensation

      • He Jifeng

      Pages 15-36

4. Tools and Applications in Industrial Software Quality Control

   1. Animating Event B Models by Formal Data Models

      • Idir Ait-Sadoune, Yamine Ait-Ameur

      Pages 37-55

   2. Automated Formal Testing of C API Using T2C Framework

      • Alexey V. Khoroshilov, Vladimir V. Rubanov, Eugene A. Shatokhin

      Pages 56-70

5. Introduction of Multi-core Systems in Automotive Applications

   1. Tailoring and Optimising Software for Automotive Multicore Systems

      • Torsten Polle, Michael Uelschen

      Pages 71-81

   2. Fault Handling Approaches on Dual-Core Microcontrollers in Safety-Critical Automotive Applications

      • Eva Beckschulze, Falk Salewski, Thomas Siegbert, Stefan Kowalewski

      Pages 82-92

   3. Timing Validation of Automotive Software

      • Daniel Kästner, Reinhard Wilhelm, Reinhold Heckmann, Marc Schlickling, Markus Pister, Marek Jersak et al.

      Pages 93-107

6. Model-Driven SOA

   1. Towards Using Reo for Compliance-Aware Business Process Modeling

      • Farhad Arbab, Natallia Kokash, Sun Meng

      Pages 108-123

   2. On the Risk Management and Auditing of SOA Based Business Processes

      • Bart Orriens, Willem-Jan v/d Heuvel, Mike Papazoglou

      Pages 124-138

   3. SCA and jABC: Bringing a Service-Oriented Paradigm to Web-Service Construction

      • Georg Jung, Tiziana Margaria, Ralf Nagel, Wolfgang Schubert, Bernhard Steffen, Horst Voigt

      Pages 139-154

7. Applications of Formal Approaches to Service-Oriented Computing

   1. A Use-Case Driven Approach to Formal Service-Oriented Modelling

      • Laura Bocchi, José Luiz Fiadeiro, Antónia Lopes

      Pages 155-169

   2. Sensoria Patterns: Augmenting Service Engineering with Formal Analysis, Transformation and Dynamicity

      • Martin Wirsing, Matthias Hölzl, Lucia Acciai, Federico Banti, Allan Clark, Alessandro Fantechi et al.

      Pages 170-190

   3. Safety and Response-Time Analysis of an Automotive Accident Assistance Service

      • Ashok Argent-Katwala, Allan Clark, Howard Foster, Stephen Gilmore, Philip Mayer, Mirco Tribastone

      Pages 191-205

   4. A Framework for Analyzing and Testing the Performance of Software Services

      • Antonia Bertolino, Guglielmo De Angelis, Antinisca Di Marco, Paola Inverardi, Antonino Sabetta, Massimo Tivoli

      Pages 206-220

   5. A Framework for Contract-Policy Matching Based on Symbolic Simulations for Securing Mobile Device Application

      • Paolo Greci, Fabio Martinelli, Ilaria Matteucci

      Pages 221-236

8. Trustworthy Computing: Theories, Methods, Tools and Experience in China and South East Asia

   1. ASERE : Assuring the Satisfiability of Sequential Extended Regular Expressions

      • Naiyong Jin, Huibiao Zhu

      Pages 237-251

   2. Computing Must and May Alias to Detect Null Pointer Dereference

      • Xiaodong Ma, Ji Wang, Wei Dong

      Pages 252-261

   3. A Partial Order Reduction Technique for Parallel Timed Automaton Model Checking

      • Zhao Jianhua, Wang Linzhang, Li Xuandong

      Pages 262-276

This volume contains the conference proceedings of ISoLA 2008, the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, which was held in Porto Sani (Kassandra, Chalkidiki), Greece during October 13–15, 2008, sponsored by EASST and in cooperation with the IEEE Technical Committee on Complex Systems. Following the tradition of its forerunners in 2004 and 2006 in Cyprus, and the ISoLA Workshops in Greenbelt (USA) in 2005 and in Poitiers (France) in 2007, ISoLA 2008 provided a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools and methods for the specification, analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their different application domains. Thus, the ISoLA series of events serves the purpose of bridging the gap between designers and developers of rigorous tools, and users in engineering and in other disciplines, and to foster and exploit synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers in companies and organizations. In p- ticular, by providing a venue for the discussion of common problems, requirements, algorithms, methodologies, and practices, ISoLA aims at supporting researchers in their quest to improve the utility, reliability, flexibility, and efficiency of tools for building systems, and users in their search for adequate solutions to their problems.

• LA
• Open Source
• design patterns
• formal models
• performance
• process modeling
• reliability
• requirements
• response-time
• risk management
• timing analysis
• ubiquitous computing
• validation
• verification

• Universität Potsdam, Potsdam, Germany

  Tiziana Margaria

• Technische Universität Dortmund, Dortmund, Germany

  Bernhard Steffen

Policies and ethics