Published: 7th September 2017|
|Invited Presentation: Traffic Sequence Charts - A Formal Visual Specification Language for Requirement Capture and Specification Development of Highly Autonomous Cars Werner Damm||1|
|Causality-Aided Falsification Takumi Akazaki Mr., Yoshihiro Kumazawa Mr. and Ichiro Hasuo Dr.||3|
|Towards Proving the Adversarial Robustness of Deep Neural Networks Guy Katz, Clark Barrett, David L. Dill, Kyle Julian and Mykel J. Kochenderfer||19|
|Game Theory Models for the Verification of the Collective Behaviour of Autonomous Cars László Z. Varga||27|
|A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification Lucas E. R. Fernandes, Vinicius Custodio, Gleifer V. Alves and Michael Fisher||35|
|Monitoring of Traffic Manoeuvres with Imprecise Information Heinrich Ody||43|
|Imperfect Knowledge in Autonomous Urban Traffic Manoeuvres Maike Schwammberger||59|
|Run-Time Risk Mitigation in Automated Vehicles: A Model for Studying Preparatory Steps Mario Gleirscher||75|
|Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System Benjamin Martin, Khalil Ghorbal, Eric Goubault and Sylvie Putot||91|
These are the proceedings of the workshop on Formal Verification of Autonomous Vehicles, held on September 19th, 2017 in Turin, Italy, as an affiliated workshop of the International Conference on integrated Formal Methods (iFM 2017). The concept of autonomy is increasingly used in vehicles of all kinds, from planes to cars. Furthermore, the degree of autonomy in these vehicles is escalating, e.g., from driver assistance systems in cars which may only act in specific situations to fully autonomous cars. Due to this increase and the potential risk involved, the correct functionality of autonomous vehicles (AV) is of utmost importance. This includes both the absence of unwanted behaviour (safety), as well as ensuring that vehicles perform wanted actions (liveness). Current methods for verification of AVs' decisions and control systems are predominantly simulation and testing based approaches. However, performing simulation and testing even on a large set of scenarios might not cover corner cases. Formal verification guarantees that such corner cases are explored in all possible ways and is hence inevitable for AVs to become a widespread technology. Advancing the current formal verification methodologies for autonomous vehicles presents significant new challenges, particularly due to the complex integration of discrete and continuous controllers of AVs. The main challenges associated with the formal design of autonomous vehicles includes modelling, specification, verification and synthesis. The workshop aim is to bring together researchers from the formal verification community that are developing formal methods for autonomous vehicles as well as researchers working, e.g., in the area of control theory or robotics, interested in applying verification techniques for designing and developing of autonomous vehicles.
The Programme Committee consisted of
We solicited both full-length papers and short papers for submission. From seven submitted full papers, five were accepted, while all of the three submitted short papers were accepted. Each submission was reviewed by at least two reviewers. The papers presented in this volume include formal approaches for
In addition to the contributed papers, the workshop featured an invited talk by Werner Damm, OFFIS Oldenburg, entitled Traffic Sequence Charts - a formal visual specification languages for requirement capture and specification development of highly autonomous cars.
We thank all the authors who submitted papers for considerations. Thanks go also to our invited speaker, Werner Damm. We are also very grateful to the members of the Programme Committee and additional external experts for their careful reviews.
It is well known that traditional approaches for type homologation fail for highly autonomous vehicles due to the impossibility of covering sufficiently many kilometers in field testing to achieve a statistically valid basis for building safety cases, due to the extreme variability of environmental contexts and the resulting complexity in both the perception- and trajectory planning systems of highly autonomous vehicles. An approach followed by automotive industry builds on scenario catalogs to capture for all perceivable traffic situations requirements on such systems jointly ensuring global safety objectives. Test drives are to be replaced to a significant extent by placing the vehicle under test in test environments exposing the vehicle to traffic situations covering all scenarios of the scenario catalog, and monitoring compliance of the vehicles reaction to such scenarios. Such test environments will allow to test separately the perception components (along all stages covering preprocessed sensor data, sensor fusion, object identification algorithms) and the trajectory planning component (which involves exploring possible future evolutions of the currently perceived traffic situations to decide on the planned maneuver). Projects already running and pushing this approach are the Pegasus project funded by the German Federal Ministry for Economic Affairs and Energy, involving all major German OEMs and Tier 1 companies, and the ENABLE-S3 Project funded by the Joint Undertaking ECSEL, including both German and French automotive companies, and covering additionally other domains for building test environments for autonomous systems, such as maritime and rail. OFFIS participates in both these projects and is involved in the planning of follow-up projects pushing a fast implementation of this approach.
There are several challenges which must be addressed to make this approach viable:
All these challenges can only be addressed if using a language for capturing scenarios, which is intuitively easy to understand, and, most prominently, which is equipped with a formal (declarative) semantics.
The talk introduces the visual specification language of Traffic Sequence Charts, which inherits key features from its parent, Live Sequence Charts, introduced jointly with D. Harel, sketches its formal semantics, and explains how they can be used to adress challenges C1-C4 above.
This research is joint work with Astrid Rakow, Carl von Ossietzky Universität Oldenburg, and Eike Möhlmann and Thomas Peikenkamp, both at OFFIS.