A Case Study on Improving the Software Dependability of a ROS Path Planner for Steep Slope Vineyards

Software for robotic systems is becoming progressively more complex despite the existence of established software ecosystems like ROS, as the problems we delegate to robots become more and more challenging. Ensuring that the software works as intended is a crucial (but not trivial) task, although proper quality assurance processes are rarely seen in the open-source robotics community. This paper explains how we analyzed and improved a specialized path planner for steep-slope vineyards regarding its software dependability. The analysis revealed previously unknown bugs in the system, with a relatively low property specification effort. We argue that the benefits of similar quality assurance processes far outweigh the costs and should be more widespread in the robotics domain.

Property Checking with Interpretable Error Characterization for Recurrent Neural Networks

This paper presents a novel on-the-fly, black-box, property-checking through learning approach as a means for verifying requirements of recurrent neural networks (RNN) in the context of sequence classification. Our technique steps on a tool for learning probably approximately correct (PAC) deterministic finite automata (DFA). The sequence classifier inside the black-box consists of a Boolean combination of several components, including the RNN under analysis together with requirements to be checked, possibly modeled as RNN themselves. On one hand, if the output of the algorithm is an empty DFA, there is a proven upper bound (as a function of the algorithm parameters) on the probability of the language of the black-box to be nonempty. This implies the property probably holds on the RNN with probabilistic guarantees. On the other, if the DFA is nonempty, it is certain that the language of the black-box is nonempty. This entails the RNN does not satisfy the requirement for sure. In this case, the output automaton serves as an explicit and interpretable characterization of the error. Our approach does not rely on a specific property specification formalism and is capable of handling nonregular languages as well. Besides, it neither explicitly builds individual representations of any of the components of the black-box nor resorts to any external decision procedure for verification. This paper also improves previous theoretical results regarding the probabilistic guarantees of the underlying learning algorithm.

Learning Interpretable Models in the Property Specification Language

We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic PSL (Property Specification Language). Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in LTL, whereas it is easy to express such properties in PSL. Moreover, formulas in PSL can be more succinct and easier to interpret (due to the use of regular expressions in PSL formulas) than formulas in LTL. The learning algorithm we designed, builds on top of an existing algorithm for learning LTL formulas. Roughly speaking, our algorithm reduces the learning task to a constraint satisfaction problem in propositional logic and then uses a SAT solver to search for a solution in an incremental fashion. We have implemented our algorithm and performed a comparative study between the proposed method and the existing LTL learning algorithm. Our results illustrate the effectiveness of the proposed approach to provide succinct human-interpretable descriptions from examples.

Checking Application Level Properties Using Assertion Synthesis

This work presents a proof-of-concept of a new approach on automatic generation of digital hardware that is able to check application-level properties of an embedded system such as a faulty system behavior at runtime. The approach makes use of assertion-based verification setups that today are very common in the area of digital hardware design with, however, the sole focus on logic simulation. Thus, a PSL-to-VHDL compiler is introduced that generates VHDL (Very High Speed Integrated Circuit Description Language) code out of PSL (Property Specification Language) assertions which can be further processed by a traditional digital logic synthesis tool. That way, runtime checker units can be automatically generated with little effort because of the already existing assertion-based test benches. Furthermore, a model railway demonstrator is presented herein as an example for a safety-critical application to prove the proposed tool flow on a use case. Implementation results based on that use case are discussed. Finally, the paper concludes with a brief outlook on related future work of the authors.