ABSTRACT. Manually designing control logic for reactive systems is time-consuming and error-prone. An alternative is to automatically generate controllers using ``correct-by-construction'' synthesis approaches. Recently, there has been interest in synthesis from Generalized Reactivity(1) or GR(1) specifications, since the required computational complexity is relatively low, and several tools exist for synthesis from GR(1) specifications. However, while these tools implement synthesis approaches that are theoretically ``correct-by-construction,'' errors in tool implementation can still lead to errors in synthesized controllers. We are therefore interested in ``end-to-end'' verification of synthesized controllers with respect to their original GR(1) specifications. Toward this end, we have modified Salty -- a tool that produces executable software implementations of controllers from GR(1) specifications in a variety of programming languages -- to produce implementations in SPARK. SPARK is both a programming language and associated set of verification tools, so it has the potential to enable the ``end-to-end'' verification we desire. In this paper, we discuss our experience to date using SPARK to implement controllers and verify them against a subset of properties comprising GR(1) specifications, namely system initial and system transition properties. We also discuss lessons learned about how to best encode controllers synthesized from GR(1) specifications in SPARK for verification, examples in which verification found unexpected controller behaviors, and caveats related to the interpretation of GR(1) specifications.

ABSTRACT. Themulus is a formal language capable of reasoning about contracts. It uses deontic logic operators as well as temporal constraints. In this paper, we study how to use Themulus to support the runtime monitoring of contracts. We present a plane boarding system as a case study. Our implementation of the monitor successfully and correctly monitors the case study with reasonable processing costs.

ABSTRACT. We present FoxDec: an approach to C code decompilation that aims at producing sound and recompilable code. Formal methods are used during three phases of the decompilation process: control flow recovery, symbolic execution, and variable analysis. The use of formal methods minimizes the trusted code base and ensures soundness: the extracted C code behaves the same as the original binary. Soundness and recompilablity enable C code decompilation to be used in the contexts of binary patching, binary porting, binary analysis and binary improvement, with confidence that the recompiled code’s behavior is consistent with the original program. We demonstrate that FoxDec can be used to improve execution speed by recompiling a binary with different compiler options, to patch a memory leak with a code transformation tool, and to port a binary to a different architecture. FoxDec can also be leveraged to port a binary to run as a unikernel, a minimal and secure virtual machine usually requiring source access for porting.

ABSTRACT. Go is an open source programming language developed at Google. We discovered a discrepancy between the Go memory model and the Go data-race detector implementation. This discrepancy leads to the under-reporting of data races in Go programs. Working with the Go community, we implemented a fix that is being incorporated into the language sources. In previous works, we had presented formalizations for a weak memory model and a data-race detector inspired by the Go specification. Is this paper, we describe how our theoretical research guided us in the process of finding and fixing a concrete bug in real-world software that powers infrastructure used by millions of people.

ABSTRACT. The increasing dependability requirements and hardware diversity of the IoT pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for RTOSs, automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.

ABSTRACT. Stability is a fundamental requirement of dynamical systems. Most of the works concentrate on verifying stability for a given stability region. In this paper we tackle the problem of synthesizing P-stable abstractions. Intuitively, the P-stable abstraction of an open dynamical system characterizes the transitions between stability regions in response to external inputs. The stability regions are not given - rather, they are synthesized as the tightest representation with respect to a given set of relevant predicates P. A P-stable abstraction is enriched by timing information derived from the duration of stabilization.

We implement a synthesis algorithm in the framework of abstract interpretation, that allows different degrees of approximation. We show the representational power of P-stable abstractions, that provide a high-level account of the behavior of the system with respect to stability, and we experimentally evaluate the effectiveness of a compositional approach, that allows synthesizing P-stable abstractions for significant systems.

ABSTRACT. We present a model-driven approach for the creation of formally verified scenarios involving human-robot interaction in healthcare settings. The work offers an innovative take on the application of formal methods to human modeling, as it incorporates physiology-related aspects. The model, based on the formalism of Hybrid Automata, includes a stochastic component to capture the variability of human behavior, which makes it suitable for Statistical Model Checking. The toolchain is meant to be accessible to a wide range of professional figures. Therefore, we have laid out a user-friendly representation format for the scenario, from which the full formal model is automatically generated and verified through the Uppaal tool. The outcome is an estimation of the probability of success of the mission, based on which the user can refine the model if the result is not satisfactory.

ABSTRACT. Along with the actively progressing field of autonomous ground and aerial vehicles, the advent of autonomous vessels has brought up new research and technological problems originating from the specifics of marine navigation. Autonomous ships are expected to navigate safely and avoid collisions following accepted navigation rules. Trustworthy navigation of autonomous ships presumes to apply provably correct navigation algorithms and control strategies. We introduce the notion of maritime game as a special case of Stochastic Priced Timed Game and model the autonomous navigation using UPPAAL STRATEGO. The navigation control strategy is optimised and verified to achieve the goal to safely reach the manoeuvre target points at a minimum cost. The approach is illustrated with the case study inspired by COLREG Rule 15.