ABSTRACT. Verifying that autonomous space robotic software behaves correctly is crucial, particularly since such software is often mission-critical where a software failure can lead to mission failure. In this paper, we describe the process that we used to verify the autonomous grasp generation and capturing operation of a spent rocket stage in space. This paper summarises a publication by the same authors in the journal Frontiers in Robotics and AI (2022) which harnesses multiple formal and non-formal methods to verify an autonomous grasping system.

ABSTRACT. Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, their real-world implementations are not regularly verified. In this paper, we present the first case study of a formal investigation of the IdentityHashMap class in the Java SDK. We specified its behavior using the Java Modeling Language (JML) and proved consistency for the main insertion and lookup methods of the implementation with respect to this specification using KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how the result of unit tests and bounded model checking can be exploited early in the specification process to come up with a suitable specifications more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementation regarding their verifiability.

ABSTRACT. Software verification allows one to examine the reliability of software. During verification, analyses often exchange information to become more effective, more efficient, or to eliminate false results and increase trust in the analysis result. One type of information that analyses provide are precisions, which describe the abstraction level (tracked predicates, etc.) of an analysis. So far, analyses mainly reuse their own precision to efficiently reverify a modified program. In contrast, we aim to reuse a precision of a predicate analysis within a value analysis. To this end, we suggest several options to convert a predicate precision into a precision for value analysis. All options compute precisions with different degrees of abstraction. We extensively evaluate our options on three applications (cooperative verification, result validation, and regression verification) and compare them against using the coarsest and finest precision as well as a state-of-the-art approach for each application. Our evaluation results indicate that coarser precisions work better for proof detection, while finer, more detailed precisions perform better in alarm detection. We also show that reusing a predicate precision in value analysis can be beneficial in cooperative verification and works well for validating and reverifying programs without property violations.

ABSTRACT. The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function, such as non-interference, continuity, or monotonicity. They can also relate calls to different functions, for instance to show that an optimized implementation is equivalent to its original counterpart. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Self-composition has been proposed to overcome this limitation, but the simplicity of its principle comes at the cost of complex transformations for non-trivial examples. We propose in this paper an alternative approach that is not based on code transformation. Instead, we show how to directly use a verification condition generator to produce logical formulas that must be verified to ensure a given relational property holds. The approach has been fully formalized and proved sound in the Coq proof assistant.

ABSTRACT. The development of cyber-physical systems has become one of the biggest challenges in the field of model-based system engineering. The difficulty stems from the complex nature of cyber-physical systems which have deeply intertwined physical processes, computation and networking system aspects. To provide the highest level of assurance, cyber-physical systems should be modelled and reasoned about at a system-level as their safety depends on a correct interaction between different subsystems. In this paper, we present a development framework of cyber-physical systems which is built upon a refinement and proof based modelling language - Event-B and its extension for modelling hybrid systems. To improve the level of automation in the deductive verification of the resulting hybridised Event-B models, the paper describes a novel approach of integrating reachability analysis in the proof process. Furthermore, to provide a more comprehensive cyber-physical system development and simulation-based validation, we describe mechanism for translating Event-B models of cyber-physical systems to Simulink. The process of applying our framework is described by using a water-tank model and then evaluated it by formally modelling and verifying a cyber-physical railway signalling system.

ABSTRACT. A lot of techniques try to improve the performance of explicit state model checking. Some techniques, like partial order reduction, are hard to apply effectively to high-level models, while others, like symmetry reduction, rarely apply to more complex real-life models. In this paper we present two techniques-state compression and operation caching-that are applicable to a wide range of models. These techniques were implemented in the ProB model checker and are available for B, Event-B, TLA+, Z and CSP-B models. The combination of both techniques is surprisingly effective, reducing both memory consumption and runtimes on a set of benchmark programs. The techniques were inspired by the success of previous work integrating LTSMin and ProB. Earlier attempts of integrating the LTSMin techniques directly into ProB (to overcome limitations of the LTSMin integration) were not successful. Similarly, earlier attempts of making the LTSMin integration available to a wider range of models (e.g., combined CSP-B models) were also not fruitful.