FormaliSE '18- Proceedings of the 6th Conference on Formal Methods in Software Engineering

How do we ensure that self-driving cars, nuclear power plants and Internet-of-things devices are safe and reliable? That is the topic of risk management. Fault tree analysis is a very popular technique here, deployed by many institutions like NASA, ESA, Honeywell, Ford, Airbus, the FDA, Toyota, Shell etc.

In this presentation, I will elaborate how the deployment of stochastic model checking can improve the capabilities of fault tree analysis, making them more powerful, flexible and efficient, allowing one to analyze a richer variety of questions faster, and thereby increasing their practical relevance and deployment in practical risk assessments.

I will report on our experience with the application and validation of these techniques in industrial practice. In particular, I will show how compositionally, model-driven engineering, graph rewriting all helped to crunch industrial cases. Finally, I will present some new directions on the deployment of big data analytics within fault tree analysis.

Software constitutes a major part of the development of robotic and autonomous systems and is critical to their successful deployment in our everyday life. Robotic software must thus run and perform as specified. Since most of these systems are used in a hard real-time context, the schedulability of their tasks is a crucial property. In this work, we propose to use formal methods to check whether the tasks of a robotic application are schedulable with respect to a given hardware platform. For this, we automatically translate functional components specified in GenoM into FIACRE, a formal language for timed systems. The generated models integrate realistic real-time schedulers based on the FCFS and the SJF cooperative policies. We use then the model-checker TINA to assert schedulability properties. We carry out experiments on a real robotic system, namely a quadcopter flight controller. We demonstrate that, on its actual hardware, schedulability properties can be formally expressed and verified. We give examples on how we can check other important behavioral and timed properties on the same synthesized models.

This article proposes a temporal and parametric specification language (PARTRAP) developed for the verification of execution traces. The language extends specification patterns with nested scopes, real-time and first-order quantification over the data inside a JSON trace, while remaining pragmatic. Its design was directed by a case study in the medical field (computer aided surgery). The paper briefly presents the case study and details the design rationale, syntax and semantics of the language. The language has been implemented and several properties have been successfully evaluated over a corpus of 100 surgery traces.

In this paper, we consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. In this paper, we present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised. We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring.

Test driven development (TDD) is a technique where test cases are used to guide the development of a system. This technique introduces several advantages at the time of developing a system, e.g. writing clean code, good coverage for the features of the system, and evolutionary development. In this paper we show how the capabilities of a testing focused development methodology based on TDD and model-based testing, can be enhanced by integrating static and runtime verification into its workflow. Considering that the desired system properties capture data- as well as control-oriented aspects, we integrate TDD with (static) deductive verification as an aid in the development of the data-oriented aspects, and we integrate model-based testing with runtime verification as an aid in the development of the control-oriented aspects. As a result of this integration, the proposed development methodology features the benefits of TDD and model-based testing, enhanced with, for instance, early detection of bugs which may be missed by TDD, regarding data aspects, and the validation of the overall system with respect to the model, regarding the control aspects.

A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall process of translation and analysis is fast, scales up to industrial programs, and introduces a negligible number of false alarms. The main result of this work is to leverage existing, mature, and sound analyzers for Java bytecode by applying them to the (translated) CIL bytecode.

Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is not necessarily a valid time representation. Current approaches to automatically detect errors in programs, such as Randoop and FindBugs, cannot detect such errors because they treat timestamps as normal integer variables and test them with random values verifying if the program throws an exception. In this paper, we present an approach that considers the time semantics of the Java language to systematically detect time related errors in Java programs. With the formal time semantics, our approach determines which integer variables handle time and which statements use or alter their values. Based on this information, it translates these statements into an SMT model that is passed to an SMT solver. The solver formally verifies the correctness of the model and reports the violations of time properties in that program. For the evaluation, we have implemented our approach in a prototype tool and applied it to the source code of 20 Java open source projects. The results show that our approach is scalable and it is capable of detecting time errors precisely enough allowing its usability in real-world applications.

We apply an IDE for user-level process design and composition to a real-life case study: a complex workflow from an ongoing global cancer-related cachexia research project. Originally buried in a manually operated spreadsheet, the process is now fully automated and integrated into the project database, ensuring the immediate availability, consistency and reproducibility of the outcomes. Our integrated solution enables the scientists to immediately execute the processes and easily customize both processes and data model to continuously changing experimental setups. The data modeling is provided by the Dynamic Web Application framework and the process modeling functionalities by the Java Application Building Center, both following the paradigm of eXtreme Model-Driven Design for model-driven software development.

Self-adaptive systems aim to efficiently respond to a wide range of changes in their operational environment by dynamically altering their behaviour. Such systems are typically comprised of a base system, implementing core functionality, and an adaptation decision process, which determines how the base system must change at different points in its execution. These two components coordinate through a set of adaptation events: a set of execution points of the former where the latter is invoked. The pattern of these events is crucial for the overall system to achieve (a) correctness against specific requirements, and (b) efficiency of system resources. Existing techniques for modelling self-adaptive systems usually hardcode adaptation events within the base system or the adaptation decision process. This limits system designers in discovering correct and optimal patterns of adaptation events, as changing those involves significant changes in the model. In this work we present Self-Adaptive Automata, an abstract modelling framework which decouples adaptation event patterns from the descriptions of base systems and adaptation decision processes. In our framework, base systems expose execution points where adaptation may happen---in the most general case this can include all system states---and adaptation decision processes are parametric to these points. A distinct automaton then pinpoints when in the system adaptation must happen. Using this framework system designers can experiment with different adaptation event patterns, without modifications to the base system or the adaptation decision process, and discover correct and efficient patterns. We show that our framework is compatible with traditional verification tools by providing an adequate translation from Self-Adaptive Automata into FDR, in which correctness against requirements can be verified. We also prove that, although our automata framework includes dynamic self-modifying features, it corresponds to standard models of computation. We illustrate the use of our framework through a use case of a self-adaptive system of autonomous search-and-rescue rovers.

In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks autonomously, the machines are equipped with different features, such as position localization, human and obstacle detection, collision avoidance, etc. Such systems are safety critical, and should operate autonomously with very high dependability (e.g., by meeting task deadlines, avoiding (fatal) accidents at all costs, etc.).

An Autonomous Wheel Loader is a machine that transports materials within the construction site without a human in the cab. To check the dependability of the loader, in this paper we provide a timed automata description of the vehicle's control system, including the abstracted path planning and collision avoidance algorithms used to navigate the loader, and we model check the encoding in UPPAAL, against various functional, timing and safety requirements. The complex nature of the navigation algorithms makes the loader's abstract modeling and the verification very challenging. Our work shows that exhaustive verification techniques can be applied early in the development of autonomous systems, to enable finding potential design errors that would incur increased costs if discovered later.

The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represent a great challenge for car manufacturers. Furthermore, we expect that in the near future, authorities require a software certification in order to get convinced that ADAS are safe enough. Theoretical research and experience show that when using conventional design approaches it is impossible to guarantee high confidence to those systems. The way taken by some industries (e.g. aerospace, railway, nuclear) was by partially using formal verification techniques.

In this paper, we first present a background of the formal verification techniques and how they can contribute to achieve the requirements of some safety standards. Next, we share our experience with the application of those techniques that seem to be mature enough to be used in an industrial context: Static analysis based on Abstract Interpretation, SMT-based software Model checking and Deductive proof. Finally, we make a detailed analysis about our experiments and propose an approach introducing formal methods into the development of automotive embedded software.