Transcript
The long road from proof of concept to real-world autonomous driving
dr. ir. Karel Van Oudheusden
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety and security Conclusion
Altreonic Provides solutions for trustworthy systems engineering: – VirtuosoNext Designer, a safe and secure distributed RTOS with programming tools – GoedelWorks, a portal based environment to support Software Engineering, with embedded certification Enabling advantage for the novel e-vehicle Kurt
Kurt Gödel (1906 – 1978)
Kurt Gödel
Altreonic’s KURT vehicle platforms
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety and security Conclusion
Engineering a safer world • What is safety? • Absence of physical harm (being hurt of killed) • No loss of mission •… • What is security? • Prevent maliciously injected fault, which causes harm • Protection of sensitive data •… • Security is a subcase of safety • Safety includes man-machine interface issues
Kurt roadmap: step by step 1. Redundant architecture • Only with electric propulsion! • Steer by wire 2. Obstacle detection/avoidance 3. Remote steering 4. Verified application software 5. Semi-autonomous driving: • Supervised, controlled environment 6. Fully autonomous: maybe never?
Kurt’s Remote Steering App Manoeuvring by smartphone Steer by web: Camera input from Kurt
Operator steers using web client
Limited speed and acceleration Authentication
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety and security Conclusion
Hazard Outdated steering commands, sent from the remote-control device to the Kurt are not discarded, causing undesired & unpredictable system behaviour.
Hazard Outdated steering commands, sent from the remote-control device to the Kurt are not discarded, causing undesired & unpredictable system behaviour.
Additional Specification The Kurt shall not execute outdated steering commands.
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety and security Conclusion
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety and security (mCRL2, …) Conclusion
mCRL2
mCRL2 L || K
mCRL2 L || K L = inL . LWait(MAX1) + listen . L LWait(0) = i . L LWait(0 < n) = i . LWait(n-1) + listen . (i + i . request) . L [0, 1]
mCRL2 L || K L = inL . LWait(MAX1) + listen . L LWait(0) = i . L
K = inK . (i + i . broadcast) . KWait(MAX2) + advice.K [0,1]
LWait(0 < n) = i . LWait(n-1) + listen . (i + i . request) . L KWait(0) = i . K [0, 1] KWait(0 < n) = i . KWait(n-1) + advice . K [0, 1]
“Outdated” #1
“Outdated” #2
“Outdated” #3
Additional Specification The Kurt shall not execute outdated steering commands.
Conceptual Clarity Three notions of “outdated” steering commands.
Additional Specification The Kurt shall not execute outdated steering commands.
Conceptual Clarity Three notions of “outdated” steering commands.
Did we Cover All Notions of “Outdated”?
Denial of Service Attack New Hazard
New Hazard New Specification An Authentic Listener cannot send two consecutive steering requests to the Kurt without receiving an intermediate broadcast message from the Kurt.
New Hazard New Specification An Authentic Listener cannot send two consecutive steering requests to the Kurt without receiving an intermediate broadcast message from the Kurt.
[true* . cLK . (!cKL)* . cLK] false
Finite State Machine
Finite State Machine [true* . cLK . (!cKL)* . cLK] false
Finite State Machine [true* . cLK . (!cKL)* . cLK] false
The property holds on the Finite State Machine
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety (mCRL2, …) Conclusion
Table of Contents 1. 2. 3. 4. 5.
Introduction Engineering a Safer World Hazard and RISK Analysis Formal modeling for safety (mCRL2, VirtuosoNext) Conclusion
Screenshot of VirtuosoNext Designer
Food for Thought • Autonomous cars connected cars wireless communication formally verified SW/HW
Food for Thought • Autonomous cars connected cars wireless communication formally verified SW/HW • Engine in conventional car = single point of failure need redundant architecture
Food for Thought • Autonomous cars connected cars wireless communication formally verified SW/HW • Engine in conventional car = single point of failure need redundant architecture • Dynamics: driver reading newspaper is a problem if he has less than 100ms to take over control supervised, controlled environments
Thank You!
karel.vanoudheusden (@) altreonic.com
