X-by-Construction: Correctness meets Probability
A track at ISoLA 2020
9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
26-30 October 2020
Aim and topics of interest |
Important dates |
Publication and special issues |
Confirmed speakers |
Track chairs |
Extended paper submission deadline: May 31, 2020
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 advertises a stepwise 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 to validate 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, the C-by-C design tools themselves, 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 2018 track “X-by-Construction” (X-by-C) with a particular emphasis on security-by-construction, we again aim to bring together researchers and practitioners that are interested in C-by-C and X-by-C. In line with the growing attention to fault-tolerance (thanks to increasingly common failures in hardware and software) and the increasing use of machine learning techniques in modern software systems — in both of these contexts, guaranteed properties are hard to establish — we want to particularly emphasise X-by-C in the setting of probabilistic properties.
We therefore invite researchers and practitioners from (at least) the following communities to share their views 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 potentially probabilistic 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 systems involving components that employ machine learning (ML) or other artificial intelligence (AI) approaches. In these settings, models and behaviour are typically dependent on what is learned from large data sets, and may change dynamically based on yet more data being processed. As a result, guaranteeing properties (whether correctness or nonfunctional ones) becomes hard, and probabilistic reasoning needs to be applied instead with respect to such properties for the components employing ML or AI approaches, and as a consequence, for systems involving such components as well.
- People working on generative software development, who are concerned with the automatic generation of software from specifications given in 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 certain 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.
Please submit your paper here
|May 4, 2020 May 31, 2020
|Notification of acceptance||
||June 29, 2020
||August 2, 2020
||September 1, 2020
|Symposium ISoLA 2020||
||October 26-30, 2020
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 or to Thematic Sections in the International Journal on Software Tools for Technology Transfer (STTT).
|Annabelle McIver / Carroll Morgan (Macquarie U & UNSW, Sydney, Australia)||
|Christel Baier (TU Dresden, Germany)||
|Marius Bozga (U Grenoble Alpes, France)||
|Uli Fahrenberg (LIX, Palaiseau, France)||
|Manfred Jaeger (Aalborg U, Denmark)||
|Joost-Pieter Katoen (RWTH Aachen, Germany)||
|Bettina Könighofer (TU Graz, Austria)||
|Tatjana Petrov (University of Konstanz, Germany)||
|Mirco Tribastone (IMT Lucca, Italy)||
For more information, please e-mail one of the track chairs.