X-by-Construction

A track at ISoLA 2018

8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation

8 November 2018
Limassol, Cyprus



Motivation | Aim and topics of interest | Important dates | Publication and special issues | Program | Track chairs | ISoLA 2018

MOTIVATION

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

A lot of progress has been made in this domain, implying it is time to look further than correctness and investigate a move from C-by-C to X-by-C, i.e. by considering also non-functional properties. X-by-C is thus concerned with a step-wise refinement process from specification to code that automatically generates software (system) implementations that by construction satisfy specific non-functional properties concerning security, dependability, reliability or resource/energy consumption, etc.

AIM

Building on the highly successful ISoLA 2016 track “Correctness-by-Construction and Post-hoc Verification: Friends or Foes?” which focussed on the combination of post-hoc verification with C-by-C, we decided to organise an “X-by-Construction” (X-by-C) track at ISoLA 2018, with the aim of bringing together researchers and practitioners that are interested in C-by-C and the promise of X-by-C.

We therefore invited researchers and practitioners from (at least) the following communities to shed their light on moving from C-by-C to X-by-C:

IMPORTANT DATES

Paper submission (extended) March 31, 2018 April 28, 2018 May 20, 2018
Notification of acceptance June 30, 2018
Camera-ready version August 15, 2018
Early registration August 31, 2018
Symposium ISoLA 2018 November 5-9, 2018
X-by-C track @ ISoLA 2018 November 8, 2018

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

The X-by-C track will take place on Thursday 8 November. Following a keynote, there will be 3 sessions according to the ISoLA schedule, hence the times are merely indicative for now.

Track introduction

 9:00 -  9:15   Maurice ter Beek, Loek Cleophas, Ina Schaefer and Bruce Watson:
       X-by-Construction

Keynote speaker

 9:15 - 10:30   Erik Poll (Radboud University Nijmegen, The Netherlands):
       (Some) Security by Construction through a LangSec Approach

10:30 - 11:00   Coffee break

Invited speakers

11:00 - 11:30   Einar Broch Johnsen Violet Pun (University of Oslo, Norway):
       Deployment by Construction for Multicore Architectures

11:30 - 12:00   Bernhard Steffen (TU Dortmund, Germany):
       Design for 'X' through Model Transformation

12:00 - 12:30   Gerardo Schneider (Chalmers TU, Gothenburg, Sweden):
       Is Privacy by Construction Possible?

12:30 - 14:00   Lunch

14:00 - 14:30   Reiner Hähnle Dominic Steinhöfel (TU Darmstadt, Germany):
       Modular, Correct Compilation with Automatic Soundness Proofs

14:30 - 15:00   Marieke Huisman (University of Twente, The Netherlands):
       Program Correctness by Transformation

15:00 - 15:30   Mirco Tribastone (IMT Lucca, Italy):
       Towards Software Performance by Construction

15:30 - 16:00   Coffee break

16:00 - 16:30   Dominique Méry (Loria, Nancy, France):
       Modelling by Patterns for Correct-by-Construction Process

16:30 - 17:00   Axel Legay Thomas Given-Wilson (Inria Rennes, France):
       X-by-C: Non-Functional Security Challenges

17:00 - 17:30   Ina Schaefer (TU Braunschweig, Germany):
       Towards Confidentiality-by-Construction

17:30 - 18:00   Discussion

TRACK CHAIRS

Maurice H. ter Beek ISTI-CNR, Pisa, Italy
Loek Cleophas TU Eindhoven, The Netherlands
Ina Schaefer TU Braunschweig, Germany
Bruce W. Watson Stellenbosch University, South Africa

For more information, please e-mail one of the track chairs.
Fondo