Correctness-by-Construction and Post-hoc Verification: friends or foes?

MOTIVATION

Correctness-by-Construction (CbC) sees the development of software (systems) as a true form of Engineering, with a capital 'E'. CbC advocates a step-wise refinement process from specification to code, ideally by CbC design tools that automatically generate error-free software implementations from rigorous and unambiguous specifications of requirements. Afterwards, testing only serves the purpose of validating the CbC process rather than to find bugs. (Of course, bugs might still be present outside the boundaries of the verified system: libraries, compilers, hardware, etc.)

In Post-hoc Verification (PhV), on the other hand, formal methods and tools are applied only after the (software) system has been constructed, but not during the development process. Typically, a formal specification of (an abstraction of) the implemented system describes how it should behave, after which V&V techniques like testing, bug finding, model checking, and deductive verification are used to check whether the implementation indeed satisfies the specifications and meets the user's needs. While two independent system models that are verified against each other can provide additional assurance that the designers' intentions are correctly captured, PhV is notoriously difficult to carry out.

Recently, numerous techniques and fields of application witness initiatives that attempt to integrate elements of both ends of the spectrum, with the aim of satisfying the holy grail of improving the correctness of software systems as well as their time-to-market, and to do so at a reasonable cost (e.g., Design for Verification or Lightweight Verification).

AIM

This track aims to bring together researchers and practitioners interested in the inherent "tension" that is usually felt when one tries to balance the pros and cons of CbC versus PhV.

We therefore invite researchers and practitioners from the following communities to shed their light on CbC versus PhV:

• People working in Software Product Line Engineering (SPLE), who try to lift successful formal methods and verification tools from single product (system) engineering to SPLE in order to say something about the correctness of all programs of an SPL (whose population is exponential in the number of features).
• People working in System-of-Systems Engineering (SoSE), who address the verification (correctness, but also issues like security, reliability, resilience, and sustainability) of networks of interacting legacy and new software systems.
• People working on (system) synthesis, who try to transform a logical specification into a system that is guaranteed to satisfy the specification in all possible environments.
• People working on deductive verification, who typically require a detailed understanding of why the system works correctly before actual verification to be able to express the correctness of a program as a set of verification conditions to be discharged.
• People working on 'bug-finding' lightweight verification, who trade off full functional verification for being able to deal with real-world languages and large programs as well as to avoid having to write formal specifications.
• People working on Design for Verification (DfV), mostly in hardware design, who advocate the usage of design methodologies, languages, patterns, etc., that make PhV a realistic option.

IMPORTANT DATES

PUBLICATION

The ISoLA proceedings will appear in Springer's Lecture Notes in Computer Science (LNCS) series.

SPECIAL ISSUES

Selected contributions will be invited to Innovations in Systems and Software Engineering: A NASA Journal, to Thematic Sections in the International Journal on Software Tools for Technology Transfer (STTT) or to the newly founded LNCS Transactions on Foundations for Mastering Change (FoMaC).

PROGRAM

 9:00 -  9:15   Track introduction

 9:15 - 10:30   Keynote by Bruce Watson (Stellenbosch University, South Africa):
       Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?

10:30 - 11:00   Coffee break

11:00 - 11:30   Bernhard Beckert (KIT, Karlsruhe, Germany):
       Deductive Verification of Legacy Code

11:30 - 12:00   Loek Cleophas (Umeå University, Sweden):
       Correctness-by-Construction /\ Taxonomies => Deep Comprehension of Algorithm Families

12:00 - 12:30   Jetty Kleijn (Leiden University, The Netherlands):
       Conditions for Compatibility of Components: The case of masters and slaves

12:30 - 14:00   Lunch

14:00 - 14:30   Axel Legay (Inria Rennes, France):
       A Logic for Statistical Model Checking of Dynamic Software Architectures

14:30 - 15:00   Dominique Méry (Loria, Nancy, France):
       On two Friends for getting Correct Programs: Automatically Translating Event-B Specifications to Recursive Algorithms in Rodin

15:00 - 15:30   Ina Schaefer (TU Braunschweig, Germany):
       Proof-Carrying Apps: Contract-Based Deployment-Time Verification

15:30 - 16:00   Coffee break

16:00 - 16:30   Erik de Vink (TU Eindhoven, The Netherlands):
       Supervisory Controller Synthesis for Product Lines with CIF 3

16:30 - 17:00   Dirk Beyer (LMU Munich, Germany):
       Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques

17:00 - 17:30   Discussion

TRACK CHAIRS