Speaker: Einar Broch Johnsen
Title: Asynchronous Software Evolution: Obtaining Type Safety by Combining Type Checking and Runtime Constraints
Speaker: Raphaël Jakse
Title: Interactive Runtime Verification – when Interactive Debugging meets Runtime Verification
Abstract: Runtime Verification consists in studying a system at runtime, looking for input and output events to discover, check or enforce behavioral properties. Interactive debugging consists in studying a system at runtime in order to discover and understand its bugs and fix them, inspecting interactively its internal state.
Interactive Runtime Verification (i-RV) combines runtime verification and interactive debugging.
We define an efficient and convenient way to check behavioral properties automatically on a program using a debugger. We aim at helping bug discovery and understanding by guiding classical interactive debugging techniques using runtime verification.
Verde is tool implementation of I-RV. Verde can be downloaded at: https://gitlab.inria.fr/mo
A brief tutorial for using Verde is available at https://gitlab.inria.fr/mon
The related paper is to be published at ISSRE’17 in October.
Speaker: Antoine El-Hokayem
Title: Monitoring Decentralized Specifications
Abstract: We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of the entire system. To do so, our approach introduces a data-structure that i) keeps track of the execution of an automaton, ii) has predictable parameters and size, and iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study decentralized monitorability, and present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Lastly, we introduce the THEMIS tool, which is a framework for designing such decentralized algorithms, and simulating their behavior.
THEMIS can be downloaded at: https://gitlab.inria.fr/monitoring/themis.
A demonstration of THEMIS is available at: https://gitlab.inria.fr/monitoring/themis-demo.
The related papers can be downloaded here and here.
Speaker: Walter Binder
Title: Towards Automated Workload Selection and Benchmark Synthesis from Open-source Code Repositories
Abstract: Researchers often rely on benchmarks to demonstrate feasibility or efficiency of their contributions. However, finding the right benchmark suite can be a daunting task – existing benchmark suites may be outdated, known to be flawed, or simply irrelevant for the proposed approach. Creating a proper benchmark suite is time consuming and often a thankless endeavor. This talk introduces AutoBench, an approach to help researchers find relevant workloads for their experimental evaluation needs. AutoBench relies on the huge number of open-source projects available in public repositories, and on unit testing having become best practice in software development. Using a repository crawler employing pluggable static and dynamic analyses for filtering and workload characterization, AutoBench allows users to automatically find projects with relevant workloads. In this talk, we illustrate AutoBench’s method to find, filter, and characterize real-world workloads from public open-source repositories, and show some motivating scenarios. Preliminary results towards automatic generation of benchmark suites are also presented, arguing that unit tests can provide a viable source of workloads, and that the combination of static and dynamic analyses improves the ability to identify relevant workloads that can serve as the basis for custom benchmark suites.
Speaker: Luke Chircop
Title: Exploring the Adoption of Specification Inference Technologies in Industry
Abstract: While no one doubts the importance of correct and complete specifications, many industrial systems still do not have formal specifications written out — and even when they do, it is hard to check their correctness and completeness. We explored the possibility of using invariant extraction tools such as Daikon to automatically infer specifications from using available resources like Test Suites with the goal of then translating them into Runtime Monitors hence providing an additional layer of security. A study was carried out on an industrial case study providing clear insights to the abilities and limitations of the Daikon tool along with the effectiveness of the Test Suites provided. Although a high recall value of 97.3% was observed, precision was observed to be much lower at 31%. The main cause for these observations was attributed to having very specific Test Suites that did not provide enough versatility for the tool to correctly generalise the specification. Moreover, the manner in which the industrial case study was built also negatively affected the effectiveness of the inference process. In future work, we plan to investigate which existing or new techniques (such as feedback or loop driven inference) can be used to improve the quality of the inferred specifications.
Speaker: Florian Lorber
Title: Timed Shield Synthesis
Abstract: One of the big visions of computer science is the automatic synthesis of implementations from formal models. However, synthesis of complete specifications usually does not scale. Shield synthesis focuses on a small set of important requirements and synthesizes a shield from them. The shield can monitor an implementations behavior, and override outputs which would violate the requirements. If such a fault is detected, the shield takes over full control over the outputs of the system. After an incorrect output, we assume no knowledge of the current state of the system. Thus the shield stays in control until the current state of the implementation is determined and the shield managed to create a valid sequence of outputs leading to that state.
In our current work, we apply shield synthesis in the timed setting, using timed automata for formalizing the selected requirements. We use the tool UPPAAL Tiga for generating a strategy for the shield which can lead it back to the implementations state either with a minimal number of steps, or with minimal time delay.
Speaker: André Pedro
Title: Runtime verification of hard real-time systems properties
Abstract: Runtime verification is an emerging discipline that investigates methods and tools to enable the verification of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verification leads to the explosion of states. Non-functional properties, such as the ones present in real-time systems are an ideal target for this kind of verification methodology, as are usually out of the range of the power and expressiveness of classic static analyses.
Current real-time embedded systems development frameworks lack support for the verification of properties using explicit time where counting time (i.e., durations) may play an important role in the development process.
Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTLD, we will present the synthesis mechanisms 1) for target systems as runtime monitors and 2) for SMT solvers as a way to get, respectively, a verdict at runtime and a schedulability problem to be solved before execution. The later is able to solve partially the schedulability analysis for periodic resource models and fixed priority scheduler algorithms.