ABSTRACT. Over the past few years, there has been significant progress in the various fields of software verification resulting in many useful tools and successful deployments, both academic and commercial. However much of the work describing these tools and ideas is written by and for the research community. The scale, diversity, and focus of the existing literature can act as a barrier, separating industrial users and the wider academic community from the tools that could make their work more efficient, more certain, and more productive. This paper gives a simple classification of verification techniques in terms of a pyramid and uses it to describe the six main schools of verification technologies. We have found this approach valuable and successful for building collaborations with industry as it allows us to explain the intrinsic strengths and weaknesses of various techniques and pick the right tool for any given industrial application. The model also highlights some of the cultural differences and unspoken assumptions of various areas of verification and illuminates future directions.

ABSTRACT. This tutorial provides an introduction to quantum computing with a focus on the applicability of formal methods on it. We will describe quantum circuits and convey an intuitive understanding of their inherent combinatorial nature and the resulting exponential blow-up that makes them hard to analyze. Then, we show how two automated reasoning techniques, weighted model counting and decision diagrams, can be used to solve hard analysis tasks for quantum circuits.

This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly: what is a basis of a vector space and how does a matrix act on it by matrix-vector multiplication?) and elementary complex number arithmetic are a prerequisite. The goal of the tutorial is to get the formal methods community inspired to use automated reasoning techniques to advance the development of quantum computing.

Tutorial duration: one full day.

ABSTRACT. We present support for automatic generation of simulation tests based on reactive models described in RoboChart, a domain-specific notation for verification of reactive designs of control software for robotic systems. The soundness and completeness of our approach are established using RoboChart’s process algebraic semantics, formalised in tock-CSP, a discrete-time variant of CSP.

RoboChart employs state machines enriched with time constructs and a component model to specify timed, platform-independent behavioural models. The RoboChart semantics defines processes that characterise the reactive behaviour of robotic control software through interactions representing sensor outputs and actuator inputs. Support for modelling, model checking, and test generation based on RoboChart is available via RoboTool. RoboChart is part of the RoboStar framework for design and verification of mobile and autonomous robots.

The testing theory for tock-CSP involves constructing tests from forbidden traces of a process, including input and output events and a special event, namely, tock, representing the passage of time. RoboTool automates the process of generating forbidden traces and constructing tests from them.

Simulations are widely used in robotics for early testing. While RoboChart models are reactive, however, simulations often follow an idealised cyclic paradigm. In each cycle, the simulation under test (SUT) evolves by accepting inputs, processing them, and providing outputs, infinitely fast, before advancing time to the next cycle. Our work with RoboChart involves comparing reactive and cyclic models using a conformance relation defined and formalised in tock-CSP. Test generation and execution must adapt to this notion of conformance.

In our work, we identify the reactive tests based on forbidden traces that are meaningful, define a process to convert those tests, provide an algorithm to execute the tests, and prove the soundness and completeness of our approach. The testing approach we present is a significant advancement in current testing practices within the field of robotics, where simulations are widely used.

ABSTRACT. The aim of this tutorial is twofold:

first, it explains the area of risk management and its most prominent concepts: the definition of risk, strategies for managing risk, the risk management cycle, and several related concepts.

Second, it provides a (necessarily incomplete) overview of several prominent approaches in formal methods geared toward better risk management. These methods help to make risk management more accountable: systematic, transparent, and quantitative.

ABSTRACT. Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. This paper is a tutorial on RV using Copilot, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware.

INSTALLATION

Although Copilot is based on Haskell, no knowledge of Haskell is required. For the purpose of this tutorial we will use a repository containing exercises and a Docker-based infrastructure to run them. This makes it easy and reliable to participate in the tutorial. If you are interested, it is highly recommended to execute the following steps prior to attending the tutorial:

1. Clone the repository at https://github.com/Copilot-Language/copilot-tutorial-material

2. Follow the steps in the included INSTALL.md file.

ABSTRACT. This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the Abstract State Machine formal method to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic way.

This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&V techniques and C++ code generation from models available in ASMETA to increase the quality and reliability of behavioral system models and source code.

ABSTRACT. In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification lan- guage and the Cameleer tool to conduct mostly-automated verification on OCaml code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions.

ABSTRACT. The verification of software systems often relies on a combination of formal methods, testing and simulation based approaches. Knowing what to specify for verification cannot be achieved without clear, unambiguous descriptions of the system requirements. This makes detailed requirements elicitation and formalisation a crucial step in the process. In this talk, I will share experiences from case studies where we have used NASA’s Formal Requirement Elicitation Tool (FRET) to formalise natural language requirements, enabling the use of mathematically-based techniques to guarantee that the system obeys certain properties. These formalised requirements subsequently guide the systems verification using a combination of paradigms, providing for system-level modelling and verification using model checkers and deductive verifiers. Insights gained during this process are shared, and we explore the expressiveness and the potential interoperability of these approaches.

Our experience confirms FRET’s suitability as a framework for the elicitation and understanding of requirements and for providing traceability from requirements to specification. In addition to providing requirements traceability, we have provided extensions to FRET with adaptations of software code refactoring’s for requirements, making requirements more manageable. We support this in Mu-FRET, a version of FRET which enables refactoring of requirements and proof that the refactored requirements have the same behaviour as the original requirements.