Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications

1. Front Matter

   PDF

2. Engineering Virtualized Systems

   1. Introduction to Track on Engineering Virtualized Services

      • Reiner Hähnle, Einar Broch Johnsen

      Pages 1-4

   2. Erlang-Style Error Recovery for Concurrent Objects with Cooperative Scheduling

      • Georg Göri, Einar Broch Johnsen, Rudolf Schlatte, Volker Stolz

      Pages 5-21

   3. Fault Model Design Space for Cooperative Concurrency

      • Ivan Lanese, Michael Lienhardt, Mario Bravetti, Einar Broch Johnsen, Rudolf Schlatte, Volker Stolz et al.

      Pages 22-36

   4. Programming with Actors in Java 8

      • Behrooz Nobakht, Frank S. de Boer

      Pages 37-53

   5. Contracts in CML

      • Jim Woodcock, Ana Cavalcanti, John Fitzgerald, Simon Foster, Peter Gorm Larsen

      Pages 54-73

   6. Distributed Energy Management Case Study: A Formal Approach to Analyzing Utility Functions

      • Aida Čaušević, Cristina Seceleanu, Paul Pettersson

      Pages 74-87

   7. Towards the Typing of Resource Deployment

      • Elena Giachino, Cosimo Laneve

      Pages 88-103

   8. Static Inference of Transmission Data Sizes in Distributed Systems

      • Elvira Albert, Jesús Correas, Enrique Martin-Martin, Guillermo Román-Díez

      Pages 104-119

   9. Fully Abstract Operation Contracts

      • Richard Bubel, Reiner Hähnle, Maria Pelevina

      Pages 120-134

3. Statistical Model Checking

   1. Statistical Model Checking Past, Present, and Future

      • Kim G. Larsen, Axel Legay

      Pages 135-142

   2. An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking

      • Cyrille Jegourel, Axel Legay, Sean Sedwards

      Pages 143-159

   3. A Formalism for Stochastic Adaptive Systems

      • Benoît Boyer, Axel Legay, Louis-Marie Traonouez

      Pages 160-176

   4. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models

      • Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll

      Pages 177-192

   5. Formal Analysis of the Wnt/β-catenin through Statistical Model Checking

      • Paolo Ballarini, Emmanuelle Gallet, Pascale Le Gall, Matthieu Manceny

      Pages 193-207

   6. Battery-Aware Scheduling of Mixed Criticality Systems

      • Erik Ramsgaard Wognsen, René Rydhof Hansen, Kim Guldstrand Larsen

      Pages 208-222

   7. Using Statistical Model Checking for Measuring Systems

      • Radu Grosu, Doron Peled, C. R. Ramakrishnan, Scott A. Smolka, Scott D. Stoller, Junxing Yang

      Pages 223-238

   8. Blocking Advertisements on Android Devices Using Monitoring Techniques

      • Khalil El-Harake, Yliès Falcone, Wassim Jerad, Mattieu Langet, Mariem Mamlouk

      Pages 239-253

   9. Monitoring with Data Automata

      • Klaus Havelund

      Pages 254-273

4. Risk-Based Testing

   1. Risk-Based Testing

      • Michael Felderer, Marc-Florian Wendland, Ina Schieferdecker

      Pages 274-276

The two-volume set LNCS 8802 and LNCS 8803 constitutes the refereed proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014, held in Imperial, Corfu, Greece, in October 2014. The total of 67 full papers was carefully reviewed and selected for inclusion in the proceedings. Featuring a track introduction to each section, the papers are organized in topical sections named: evolving critical systems; rigorous engineering of autonomic ensembles; automata learning; formal methods and analysis in software product line engineering; model-based code generators and compilers; engineering virtualized systems; statistical model checking; risk-based testing; medical cyber-physical systems; scientific workflows; evaluation and reproducibility of program analysis; processes and data integration in the networked healthcare; semantic heterogeneity in the formal development of complex systems. In addition, part I contains a tutorial on automata learning in practice; as well as the preliminary manifesto to the LNCS Transactions on the Foundations for Mastering Change with several position papers. Part II contains information on the industrial track and the doctoral symposium and poster session.

• automata
• automated software engineering
• autonomic systems
• business process modeling
• code generation
• component-based
• coordination patterns
• domain-specific languages
• ensemble computing
• model based testing
• model checking
• operational semantics
• prototyping
• real-time
• robot swarms
• software product lines
• timed automata
• verification

• University of Limerick, Ireland

  Tiziana Margaria

• TU Dortmund, Germany

  Bernhard Steffen

Policies and ethics