THEME AND OBJECTIVE

Formal methods have been an active research area for decades. They are considered to be one of the most effective tools to develop highly dependable software for critical applications. Although there is wide interest in applying these methods in dependable systems practice, this domain has not yet successfully adopted them. Many practitioners believe in their high potential and would use them to their maximum benefit, whether directly or through powerful tools. However, their beneficial use is still hindered, for example, by poor scalability, missing or inadequate tools, scarce teaching, and a lack of trained personnel. The lack of recent knowledge about these obstacles and formal methods effectiveness and productivity raise a high demand for formal method research and goal-directed collaborations between academia, regulators, and industry.

With this workshop, we want to strengthen the community of researchers that

  • perform evaluations of existing formal approaches and variants in practical contexts and

  • support the transfer of these methods into dependable systems practice.

TOPICS OF INTEREST

Submissions are expected to contribute to this objective by answering one or more of the following questions for the formal approach(es) under examination:

  • Approach: How can the approach be applied in practice?

  • Automation: Which tool support is proposed? If abstraction is needed to apply the approach, how is it automated?

  • Integration: If several approaches are to be applied in an integrated way; if the approach is to be used with a modelling technique or programming language; if the approach is to be integrated into an engineering process, what are the benefits?

  • Methodology: How can the approach be applied at scale, for example, using composition and refinement?

  • Transfer: How is teaching or training to be organised to transfer the approach?

  • Usefulness: How is usefulness achieved? Is the approach effective? What would have been different if a conventional or non-formal alternative was used (e.g., relative fault-avoidance or fault-detection effectiveness)?

  • Ease of Use: How is ease of use achieved? Is the approach efficient? How was its usability and maturity assessed (e.g., abstraction effort, proof complexity, productivity) and what are the results?

  • Evaluation: Why will the approach be useful for a wide range of critical applications?

Along with these questions, workshop contributions can highlight new practical challenges, important limitations, barriers, or benefits, and widely used tools and languages regarding their support of the examined approach.