From b5939bc9db42a304d5b3ec54766178b49651a896 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sat, 8 Jan 2022 22:22:22 +0100 Subject: [PATCH] added basckground chapter . First flush. --- .../2022-RAS-SI/document/root.bib | 31 +++++++++++++ .../scholarly_paper/2022-RAS-SI/paper.thy | 46 +++++++++++-------- 2 files changed, 57 insertions(+), 20 deletions(-) diff --git a/examples/scholarly_paper/2022-RAS-SI/document/root.bib b/examples/scholarly_paper/2022-RAS-SI/document/root.bib index 90938293..38fd8130 100644 --- a/examples/scholarly_paper/2022-RAS-SI/document/root.bib +++ b/examples/scholarly_paper/2022-RAS-SI/document/root.bib @@ -1298,6 +1298,37 @@ isbn="978-3-540-48509-4" location = {Paris, France} } + +@article{arXiv170806374, + author = {{Shalev-Shwartz}, Shai and {Shammah}, Shaked and {Shashua}, Amnon}, + title = "{On a Formal Model of Safe and Scalable Self-driving Cars}", + journal = {arXiv e-prints}, + keywords = {Computer Science - Robotics, Computer Science - Artificial Intelligence, Statistics - Machine Learning}, + year = 2017, + month = aug, + eid = {arXiv:1708.06374}, + pages = {arXiv:1708.06374}, +archivePrefix = {arXiv}, + eprint = {1708.06374}, + primaryClass = {cs.RO}, + adsurl = {https://ui.adsabs.harvard.edu/abs/2017arXiv170806374S}, + adsnote = {Provided by the SAO/NASA Astrophysics Data System} +} + + +@techreport{wolff:hal03429597, + title = {{Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP}}, + author = {Paolo and Taha, Safouan and Wolff, Burkhart}, + url = {https://hal.inria.fr/hal-03429597}, + type = {Research Report}, + institution = {{University Paris-Saclay ; IRT SystemX, Palaiseau}}, + year = {2021}, + month = oct, + pdf = {https://hal.inria.fr/hal-03429597/file/document.pdf}, + hal_id = {hal-03429597}, + hal_version = {v1} +} + @Book{ nipkow.ea:isabelle:2002, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/{HOL}---A Proof Assistant for Higher-Order Logic}, diff --git a/examples/scholarly_paper/2022-RAS-SI/paper.thy b/examples/scholarly_paper/2022-RAS-SI/paper.thy index 89172b43..af133f6b 100644 --- a/examples/scholarly_paper/2022-RAS-SI/paper.thy +++ b/examples/scholarly_paper/2022-RAS-SI/paper.thy @@ -13,6 +13,7 @@ declare[[ Theorem_default_class = "theorem"]] define_shortcut* csp \ \CSP\ holcsp \ \HOL-CSP\ + hol \ \HOL\ isabelle \ \Isabelle/HOL\ (*>*) @@ -56,7 +57,7 @@ text*[introtext::introduction]\ A widely accepted definition of Cyber-physical Systems (CPS) such as robots or autonomous cars would comprise the following feature-list: they are systems involving \<^item> concurrent interaction of digitally controlled actors and an environments
, -\<^item> dense time (\\0)
, +\<^item> dense time (\\\0\)
, \<^item> continuous environment with multi-dimensional observables 
 underlying the laws of (Newtonian) physics
, \<^item> the discretising view of continuous observables in @@ -74,9 +75,9 @@ Our understanding of 'analysis' of CPS involves: In this paper, we present a \<^emph>\framework\ for modeling and formally analysing CPS's and a concrete \<^emph>\instance\ in form of a case study from the autonomous car domain. The latter is concerned with the formal verification of a particular collision-avoiding driving -strategy developed by @{cite "RSS Paper"}. Roughly speaking, our framework is based on a -conservative embedding called HOL-CSP2.0 @{cite "AFP entry"} into \<^isabelle> @{cite "XXX"} -which serves both as modeling and analysis environment. +strategy developed by @{cite "wolff:hal03429597"}. Roughly speaking, our framework is based on a +conservative embedding called HOL-CSP2.0 @{cite "HOL-CSP-AFP"} into \<^isabelle> +@{cite "nipkow.ea:isabelle:2002"} which serves both as modeling and analysis environment. Describing our foundational stack in more detail, we'd like to mention: \<^item> Communicating Sequential Processes (\<^csp>), which is a language @@ -97,17 +98,20 @@ Describing our foundational stack in more detail, we'd like to mention: \<^emph>\conservative extensions\, comprise a notable amount of number theory, real analysis, and program semantics theories. +\ +text\ The expressive power of \<^holcsp> stems from the fact that its \<^emph>\channels\ may comprise arbitrary \<^hol>-types, and thus infinite data for which powerful interactive and automated proof techniques are available. In particular, CPS and \<^holcsp> fit particularly well together since: % better a presentation as table ? -\<^item> concurrent interaction of actors and environments: - this is what \<^csp> is built for; -\<^item> dense time (\\\0\): the libraries provide real numbers as well as rich theories to reason - about them; -\<^item> continuous physical environment with multi-dimensional observables - underlying the laws of (Newtonian) physics
: the Isabelle/HOL-Analysis library provides - definitions and proof techniques to reason over differential equations; + +\<^item> concurrent interaction of actors and environments: this is what \<^csp> is built for; +\<^item> dense time (\\ \ 0\): + the libraries provide real numbers as well as rich + theories to reason about them; +\<^item> continuous physical environment with multi-dimensional observables underlying the laws of + (Newtonian) physics
: the Isabelle/HOL-Analysis library provides definitions and proof + techniques to reason over differential equations; \<^item> discretized/sampled view of continuous variables: \<^hol> libraries provide theories for vector-spaces for positions, forces, accellerations, etc, as well as (low-level, machine-oriented) bitvector calculations @@ -115,20 +119,22 @@ are available. In particular, CPS and \<^holcsp> fit particularly well together can be adapted, as we will see. \ -text\This paper proceeds as follows: -after an introduction into \<^holcsp> we present the general framework of -interacting autonomous cars, which may be modeled in a object-oriented manner as -in the domain-specific ontology language Mozart @{cite "XXX"}. This involves the conception -of an orchestrator (the 'maxwell-daemon') that represents the assumption that all actors -posses "perfect" captors and 'know' at some points in time the absolute physical state -of all other actors, and that react on this knowledge by a particular non-deterministic -\<^emph>\driving strategy\. +text\This paper proceeds as follows: after an introduction into \<^holcsp> we present the general +framework of interacting autonomous cars, which may be modeled in a object-oriented manner as +in the domain-specific ontology languages such as +MOSAR \<^footnote>\\<^url>\https://www.mosar.io\\ or +Foretellix's M-SDL \<^footnote>\\<^url>\https://www.foretellix.com/open-language/\\. + +This involves the conception of an orchestrator (the 'maxwell-daemon') that represents the +assumption that all actors posses "perfect" captors and 'know' at some points in time the absolute +physical state of all other actors, and that react on this knowledge by a particular +non-deterministic \<^emph>\driving strategy\. Subsequently, inside this framework, we present a concrete topology and scenario with two or more cars on a lane, that follow the RSS driving strategy. The latter has been proposed by S. Shaliv-Shwartz, S. Shammah, A. Shashua: 
 "On a Formal Model of Safe and Scalable Self-driving Cars" -@{cite \XXX\} and which comes up with a concrete formal definition +\cite{arXiv170806374} and which comes up with a concrete formal definition compatible 
with the law ("Duty of Care"). Moreover, the authors provide a paper-and-pencil proof trying to establish a global safety property over a class of scenarios, which basically excludes the existence of collisions.