Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 18th International Conference on Software Engineering and Formal Methods, SEFM 2020, held in Amsterdam, The Netherlands, in September 2020.

The 16 full papers presented together with 1 keynote talk and an abstract of a keynote talk were carefully reviewed and selected from 58 submissions. The papers cover a large variety of topics, including testing, formal verification, program analysis, runtime verification, meta-programming and software development and evolution. The papers address a wide range of systems, such as IoT systems, human-robot interaction in healthcare scenarios, navigation of maritime autonomous systems, and operating systems.
The Chapters "Multi-Purpose Syntax Definition with SDF3", “FRed: Conditional Model Checking via Reducers and Folders" and "Difference Verification with Conditions” are available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.

Inhaltsverzeichnis

Frontmatter

Open Access

Multi-purpose Syntax Definition with SDF3

Abstract
SDF3 is a syntax definition formalism that extends plain context-free grammars with features such as constructor declarations, declarative disambiguation rules, character-level grammars, permissive syntax, layout constraints, formatting templates, placeholder syntax, and modular composition. These features support the multi-purpose interpretation of syntax definitions, including derivation of type schemas for abstract syntax tree representations, scannerless generalized parsing of the full class of context-free grammars, error recovery, layout-sensitive parsing, parenthesization and formatting, and syntactic completion. This paper gives a high level overview of SDF3 by means of examples and provides a guide to the literature for further details.
Luís Eduardo de Souza Amorim, Eelco Visser

Finding and Fixing a Mismatch Between the Go Memory Model and Data-Race Detector

A Story on Applied Formal Methods
Abstract
Go is an open-source programming language developed at Google. In previous works, we presented formalizations for a weak memory model and a data-race detector inspired by the Go specification. In this paper, we describe how our theoretical research guided us in the process of finding and fixing a concrete bug in the language. Specifically, we discovered and fixed a discrepancy between the Go memory model and the Go data-race detector implementation—the discrepancy led to the under-reporting of data races in Go programs. Here, we share our experience applying formal methods on software that powers infrastructure used by millions of people.
Daniel Schnetzer Fava

Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

Abstract
Along with the very 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 COLREG navigation rules. Trustworthy navigation of autonomous ships presumes applying 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. Furthermore, we use the refinement technique to develop a game model in a correct-by-construction manner. The navigation strategy is verified and optimized to achieve the goal to safely reach the manoeuvre target points at a minimum cost. The approach is illustrated with a case study inspired by COLREG Rule 15.
Fatima Shokri-Manninen, Jüri Vain, Marina Waldén

End-to-End Verification of Initial and Transition Properties of GR(1) Designs in SPARK

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.
Laura R. Humphrey, James Hamil, Joffrey Huguet

Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification

Abstract
We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.
Jonathan Julián Huerta y Munive

Interoperability and Integration Testing Methods for IoT Systems: A Systematic Mapping Study

Abstract
The recent active development of Internet of Things (IoT) solutions in various domains has led to an increased demand for security, safety, and reliability of these systems. Security and data privacy are currently the most frequently discussed topics; however, other reliability aspects also need to be focused on to maintain smooth and safe operation of IoT systems. Until now, there has been no systematic mapping study dedicated to the topic of interoperability and integration testing of IoT systems specifically; therefore, we present such an overview in this study. We analyze 803 papers from four major primary databases and perform detailed assessment and quality check to find 115 relevant papers. In addition, recently published testing techniques and approaches are analyzed and classified; the challenges and limitations in the field are also identified and discussed. Research trends related to publication time, active researchers, and publication media are presented in this study. The results suggest that studies mainly focus only on general testing methods, which can be applied to integration and interoperability testing of IoT systems; thus, there are research opportunities to develop additional testing methods focused specifically on IoT systems, so that they are more effective in the IoT context.
Miroslav Bures, Matej Klima, Vaclav Rechtberger, Xavier Bellekens, Christos Tachtatzis, Robert Atkinson, Bestoun S. Ahmed

Open Access

FRed: Conditional Model Checking via Reducers and Folders

Abstract
There are many hard verification problems that are currently only solvable by applying several verifiers that are based on complementing technologies. Conditional model checking (CMC) is a successful solution for cooperation between verification tools. In CMC, the first verifier outputs a condition describing the state space that it successfully verified. The second verifier uses the condition to focus its verification on the unverified state space. To use arbitrary second verifiers, we recently proposed a reducer-based approach. One can use the reducer-based approach to construct a conditional verifier from a reducer and a (non-conditional) verifier: the reducer translates the condition into a residual program that describes the unverified state space and the verifier can be any off-the-shelf verifier (that does not need to understand conditions). Until now, only one reducer was available. But for a systematic investigation of the reducer concept, we need several reducers. To fill this gap, we developed FRed, a Framework for exploring different REDucers. Given an existing reducer, FRed allows us to derive various new reducers, which differ in their trade-off between size and precision of the residual program. For our experiments, we derived seven different reducers. Our evaluation on the largest and most diverse public collection of verification problems shows that we need all seven reducers to solve hard verification tasks that were not solvable before with the considered verifiers.
Dirk Beyer, Marie-Christine Jakobs

Open Access

Difference Verification with Conditions

Abstract
Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.
Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger

A Formal Modeling Approach for Portable Low-Level OS Functionality

Abstract
The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (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.
Renata Martins Gomes, Bernhard Aichernig, Marcel Baunach

Model-Based Testing Under Parametric Variability of Uncertain Beliefs

Abstract
Modern software systems operate in complex and changing environments and are exposed to multiple sources of uncertainty. Considering uncertainty as a first-class concern in software testing is currently on an uptrend. This paper introduces a novel methodology to deal with testing under uncertainty. Our proposal combines the usage of parametric model checking at design-time and online model-based testing algorithms to gather runtime evidence and detect requirements violations. As modeling formalism, we adopt parametric Markov Decision Processes where transition probabilities are not fixed, but are possibly given as a set of uncertain parameters. The design-time phase aims at analyzing the parameter space to identify the constraints for requirements satisfaction. Then, the testing activity applies a Bayesian inference process to identify violations of pre-computed constraints. An extensive empirical evaluation shows that the proposed technique is effective in discovering violations and is cheaper than existing testing under uncertainty methods.
Matteo Camilli, Barbara Russo

Hoare-Style Logic for Unstructured Programs

Abstract
Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic \(\mathcal {L}_A\), which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of \(\mathcal {L}_A\) have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.
Didrik Lundberg, Roberto Guanciale, Andreas Lindner, Mads Dam

Synthesis of P-Stable Abstractions

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 \(\mathbb {P}\) -stable abstractions. Intuitively, the \(\mathbb {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 \(\mathbb {P}\). A \(\mathbb {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 \(\mathbb {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 \(\mathbb {P}\)-stable abstractions for significant systems.
Anna Becchi, Alessandro Cimatti, Enea Zaffanella

Runtime Verification of Contracts with Themulus

Abstract
Contracts regulating the behaviour of multiple interacting parties go beyond the notion of pure properties, but allow one to document and analyse the ideal behaviour. In this paper we build upon a real-time deontic logic allowing the description of such contracts and present a runtime verification tool for monitoring of such contracts. We present a verification algorithm used to monitor contracts written in this logic and an airport agreement is used as a case study to illustrate how such agreements and contracts can be monitored using our tool with reasonable processing costs.
Alberto Aranda García, María-Emilia Cambronero, Christian Colombo, Luis Llana, Gordon J. Pace

Sound C Code Decompilation for a Subset of x86-64 Binaries

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.
Freek Verbeek, Pierre Olivier, Binoy Ravindran

Statically Checking REST API Consumers

Abstract
Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at runtime. In this paper, we present SRS, a language that extends the support of static analysis to calls to REST services, with the ability to statically find common errors such as missing or invalid data in REST calls and misuse of the results from such calls. SRS features a syntax similar to JavaScript and is equipped with a rich collection of types and primitives to natively support REST calls that are statically validated against specifications of the corresponding APIs written in the HeadREST language.
Nuno Burnay, Antónia Lopes, Vasco T. Vasconcelos

A Layered Implementation of DR-BIP Supporting Run-Time Monitoring and Analysis

Abstract
Reconfigurable systems are emerging in many application domains as reconfiguration can be used to cope with unpredictable system environments and adapt by delivering new functionality. The Dynamic Reconfigurable BIP (DR-BIP) framework is an extension of the BIP component framework enriched with dynamic exogenous reconfiguration primitives, intended to support rigorous modeling of reconfigurable systems. We present a new two-layered implementation of DR-BIP clearly separating between execution of reconfiguration operations and execution of a fixed system configuration. Such a separation of concerns offers the advantage of using the mature and efficient BIP engine as well as existing associated analysis and verification tools. Another direct benefit of the new implementation is the possibility to monitor a holistic view of a system’s behavior captured as a set of traces involving information about both the state of the system components and the dynamically changing architecture. Monitoring and analyzing such traces poses interesting questions regarding the formalization and runtime verification of properties of reconfigurable systems.
Antoine El-Hokayem, Saddek Bensalem, Marius Bozga, Joseph Sifakis

Formal Verification of Human-Robot Interaction in Healthcare Scenarios

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.
Livia Lestingi, Mehrnoosh Askarpour, Marcello M. Bersani, Matteo Rossi

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise