ABSTRACT. Autonomous - and Robotic - Systems are systems made up of collaborating computational elements, interacting and adapting to the physical environment and making autonomous decisions. Formal methods provide mathematically-based techniques for the specification and development of software and hardware systems. The adoption of formal methods by the industry developing autonomous and robotic systems is, however, still slow. This talk reports on a two-year research collaboration with industry focused on applying formal method techniques in the development of autonomous systems. First, it discusses the main challenges and results achieved in the definition of specification patterns for robotic missions [5, 8, 6], a project in collaboration with PAL Robotics [3] and BOSCH [1]. Mission specification patterns provide logic-based solutions for recurrent specification problems where developers have to define the desired behavior of a robotic application (a.k.a missions). Then, it discusses a procedure for generating online test oracles from logic-based formulations of functional requirements of autonomous systems [7], a project in collaboration with Luxspace [2] and QRA Corp [4]. The procedure addresses a set of real-world challenges related to autonomous systems and has been evaluated on a real-world satellite system model. Finally, the talk presents a set of challenges and opportunities that emerged from the two-year journey of collaboration with industry.

References

1. BOSCH (2018), https://www.bosch.com/

2. Luxspace (2019), http://luxspace.lu/

3. PAL Robotics (2019), http://pal-robotics.com/

4. QRA corp (2019), https://qracorp.com/

5. Robotic Patterns (2019), http://roboticpatterns.com/

6. Menghi, C., Tsigkanos, C., Berger, T., Pelliccione, P., Ghezzi, C.: Poster: Prop-erty Specification Patterns for Robotic Missions. In: ICSE: Companion Proceedings(2018)

7. Menghi, C., Nejati, S., Gaaloul, K., Briand, L.C.: Generating Automated and OnlineTest Oracles for Simulink Models with Continuous and Uncertain Behaviors. In: FSE(2019)

8. Menghi, C., Tsigkanos, C., Berger, T., Pelliccione, P.: PsALM: Specification of De-pendable Robotic Missions. In: ICSE: Companion Proceedings (2019)

ABSTRACT. The design of autonomous vehicles includes obstacle detection and avoidance, route planning, speed control, etc. However, there is a gap in the representation of the rules of the road on an autonomous vehicle. 
Additionally, it is necessary to understand the behaviour of an autonomous vehicle in order to check whether or not is works according to the rules of the road. Here, we propose an agent-based architecture to embed the rules of the road into an agent representing the behaviour of an autonomous vehicle. We use temporal logic to formally represent the rules of the road in a way it should be possible to capture when and how a given rule of the road can be applied.

ABSTRACT. Ensuring pedestrian-safety is paramount to the acceptance and success of autonomous cars. The scenario-based training and testing of such self-driving vehicles in virtual driving simulation environments increasingly gained attention in the past years. Key challenge is the automated generation of critical trac scenarios which usually are rare in real-world trac, while computing and testing all possible scenarios is infeasible in practice. In this paper, we present a formal method-based approach CriSGen for an automated and complete generation of critical trac scenarios for virtual training of self-driving cars. These scenarios are determined as close variants of given but uncritical and formally abstracted scenarios via reasoning on their non-linear arithmetic constraint formulas, such that the original maneuver of the self-driving car in them will not be pedestrian-safe anymore, enforcing it to further adapt the behavior.

ABSTRACT. Nowadays, autonomous crossing manoeuvres at intersections are especially challenging. In related work, a crossing controller for provably safe autonomous urban traffic manoeuvres was introduced. We extend this controller by a decentralised scheduling mechanism that ensures fair behaviour of the controller and also guarantees bounded liveness. We verify the correctness of our extension by an implementation and analysis with UPPAAL Stratego.

ABSTRACT. Teleo-Reactive(TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. The example is sufficient to illustrate key properties that a TR and a TeleoR program should have. We give formal definitions of the key properties, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express the key properties in LTL. Finally we show how their LTL formalisation can be used to prove key properties of TeleoR procedures by using the example TeleoR program.

ABSTRACT. Real-time, on-board runtime reasoning about system safety and security is required for autonomous systems, including most everything that flies: aircraft, spacecraft, satellites, and the robotic systems therein. The field of runtime verification (RV) is vast, and quickly growing, yet when it comes to real-life autonomous systems, current RV capabilities just don't fly. There is a dearth of RV tools that can operate within the constraints of real-life embedded operations that limit the system instrumentation, space, timing, power, weight, cost, operating conditions, and other resources. Even when we devise tools for embedded operation, RV must first clear the tall hurdles of input specifications, validation, verification, and flight certification. We highlight case studies where RV has recently risen to the occasion of reasoning on-board real-life autonomous systems, such as Unmanned Aerial Systems and NASA's Robonaut2, and examine the way up from here. What will it take for RV to really take off?

ABSTRACT. Safe operation of Cyber-Physical Systems such as Unmanned Aircraft Systems requires guarantees not only on the system, but also on the mission. Following approaches that are used to produce robust Cyber-Physical Controllers, we present the architecture of a mission definition, verification and validation toolchain. We conclude by reporting on the current state of the authors' implementation of this framework.