A track at ISoLA 2018
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
8 November 2018
Aim and topics of interest |
Important dates |
Publication and special issues |
Track chairs |
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.
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:
- People working on system-of-systems, who address modelling and verification (correctness, but also non-functional properties concerning security, reliability, resilience, energy consumption, performance and sustainability) of networks of interacting legacy and new software systems, and who are interested in applying X-by-C techniques in this domain in order to prove non-functional properties of systems-of-systems by construction (from their constituent systems satisfying these properties).
- People working on quantitative modelling and analysis (e.g. through probabilistic or real-time systems and probabilistic or statistical model checking) in particular in the specific setting of dynamic, adaptive or (runtime) reconfigurable systems with variability. These people work on lifting successful formal methods and verification tools from single systems to families of systems, i.e. modelling and analysis techniques that need to cope with the complexity of systems stemming from behaviour, variability, and randomness — and which focus not only on correctness but also on non-functional properties concerning safety, security, performance or dependability properties. As such, they may be interested in applying X-by-C techniques in this domain to prove non-functional properties of families of systems by construction (from their individual family members satisfying these properties).
- People working on generative software development, who are concerned with the automatic generation of software from specifications given in either general formal languages or domain-specific languages, leading to families of related software (systems). Also in this setting, the emphasis so far has typically been on functional correctness, but the restricted scope of the specifications — especially for domain-specific languages — may offer a suitable ground for reasoning about non-functional properties, and for using X-by-C techniques to guarantee such properties.
- People working on systems security, privacy and algorithmic transparency and accountability, who care about more than correctness. The application of X-by-C techniques could provide security guarantees from the outset when designing critical systems. It could also enforce transparency when developing algorithms for automated decision-making, in particular those based on data analytics — thus reducing algorithmic bias by avoiding opaque algorithms.
|March 31, 2018 April 28, 2018 May 20, 2018
|Notification of acceptance||
||June 30, 2018
||August 15, 2018
||August 31, 2018
|Symposium ISoLA 2018||
||November 5-9, 2018
|X-by-C track @ ISoLA 2018||
||November 8, 2018
The ISoLA proceedings will appear in Springer's Lecture Notes in Computer Science (LNCS) series.
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).
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.
9:00 - 9:15 Maurice ter Beek, Loek Cleophas, Ina Schaefer and Bruce Watson:
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
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):
17:30 - 18:00 Discussion
For more information, please e-mail one of the track chairs.