Post on 17-Sep-2018
Auf dem Weg zur unbemannten Luftfracht durch sichere Software und Laufzeitabsicherung Christoph Torens, Florian Adolf, Sebastian Schirmer DLR Institut für Flugsystemtechnik, Abteilung Unbemannte Luftfahrtzeuge DGLR Workshop “Software Safety”, 5. Oktober 2016 Fachausschüsse L6.3 Flugregelung und Q3.4 Software Engineering
www.DLR.de • Chart 2 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Unbemannte Luftfracht Stand der Technik
Kaman Unmanned K-Max Militärische Anwendung
Ca. 750 h automatischer Flug
DHL Paketkopter Erprobungsphase 45 min Flugzeit 1.2 kg Nutzlast
© Lockheed Martin
© DHL
Google Project Wing Erprobungsphase Bisher Luftraum G 1.5 kg Nutzlast
© Amazon
Amazon Prime Air Erprobungsphase Höhenseparation nach Fluggeschw.
Langsam: AGL < 200ft Schnell: 200 ft < AGL <500 ft
NASA UTM Air traffic management for low altitude drones
© NASA
© Lockheed Martin
DARPA ARES Aerial Reconfigurable
Embedded System Phase III: Prototypherstellung
EASA: Concept of Operations for Drones
Direct visual line of sight < 150 m altitude Outside reserved areas
No certification
Risks like manned aviation Size, complexity, kinetic energy
Full certification
Open Category Certified Category Specific Category
?
Beyond line of sight > 150 m altitude No MTOW limit Increased Risk
Operation-based safety risk assessment
Specific Operation Risk Assessment (SORA)
𝑃𝑃𝑐𝑐𝑐𝑐𝑐𝑐𝑐𝑐𝑐 < 10−7
𝑃𝑃𝑐𝑐𝑐𝑐𝑐𝑐𝑐𝑐𝑐 < 10−3
𝑃𝑃𝑣𝑣𝑣𝑣𝑣𝑣𝑣𝑣𝑐𝑐𝑣𝑣𝑣𝑣 < 10−4
?
open certified specific
Specific Operation Risk Assessment
Direct visual line of sight
< 150 m altitude
Outside reserved areas
No certification
Risks like manned aviation
Size, complexity, kinetic energy
Full certification
Beyond line of sight > 150 m altitude Increased Risk
www.DLR.de • Chart 6 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Introduction ARTIS Fleet Autonomous Research Testbed for Intelligent Systems
miniARTIS (1.5kg) midiARTIS (14kg)
superARTIS (90-150 kg)
Prometheus (25kg)
www.DLR.de • Chart 7 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Research Focus & Challenges
DO-178C
Online Mapping Algorithms Trajectory-based Control
Online Guidance and Navigation Algorithms Assurance
MiPlEx Software Framework
www.DLR.de • Chart 8 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ALFURS Capabilities [Kendoul2012]
www.DLR.de • Chart 9 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ALFURS-based Generic Model
www.DLR.de • Chart 10 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ALFURS-based Generic Model
www.DLR.de • Chart 11 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ALFURS-based Generic Model
www.DLR.de • Chart 12 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ALFURS-based Generic Model
www.DLR.de • Chart 13 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
DO-178C Process View
• Testautomatisierung • Agile Ansätze • Metriken • Formale Methoden • DO-178C
www.DLR.de • Chart 14 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ARTIS Test Strategy [DGLR WS L6.3/Q3.4, 2013]
Formal Methods
Static Tests
Unit Tests Software-
in-the-Loop
Hardware-in-the-Loop
Flight Test
CppCheck
Static Asserts
Sensor Emulation
Closed Loop Planning &Control Use Cases / Boundary Cases
MBT, Coverage
www.DLR.de • Chart 15 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
ARTIS Test & Assurance Strategy
CppCheck
Static Asserts
Formal Methods
Static Tests
Unit Tests
Software-in-the-Loop
Hardware-in-the-Loop
Flight Test
Runtime Monitoring
Monitor
www.DLR.de • Chart 16 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Formal Methods and Requirements in DO-Stds
Requirements
Formalization
Modelling
Model-checking Certification
DO-178C
DO-331
DO-333 DO-333 DO-330
DO-178C
DO-330
DO-331
DO-333
…
DO-333
[Torens2016]
[Torens2016]
[Torens2016]
[Torens2015]
www.DLR.de • Chart 17 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Requirements
Formalization
Modelling
Model-checking
Certification DO-178C Verification Processes:
www.DLR.de • Chart 18 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Requirements Related Objectives DO-178C/333
Requirements
Formalization
Modelling
Model-checking
Certification
www.DLR.de • Chart 19 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Requirements Elicitation with Templates
• Semi-formalization of requirements • Template for engineers not familiar with requirements management • Helps to include relevant aspects • Allow full textual requirements as alternative
Requirements
Formalization
Modelling
Model-checking
Certification
Condition System / Subsystem
Obligation Action Object Additional Details
www.DLR.de • Chart 20 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Tabular Representation MiPlEx: Mission Management
Requirements
Formalization
Modelling
Model-checking
Certification
Condition System / Subsystem
Obliga-tion
Action Object / Additional Details
www.DLR.de • Chart 21 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Requirements Formalization MiPlEx: Mission Management
Certification
Requirements
Formalization
Modelling
Model-checking
Certification
* *) no actual certification was done, BUT we see that certification is reasonable using the proposed methodology
Condition System / Subsystem
Obliga-tion
Action Object / Additional Details
www.DLR.de • Chart 22 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Graphical Concept Model MiPlEx: Mission Management
Requirements
Formalization
Modelling
Model-checking
Certification
www.DLR.de • Chart 23 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
NuSMV Modelling (LTL) MiPlEx: Mission Management
Requirements
Formalization
Modelling
Model-checking
Certification
www.DLR.de • Chart 24 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Model-Checking with NuSMV MiPlEx: Mission Management
Certification
Requirements
Formalization
Modelling
Model-checking
Certification
* *) no actual certification was done, BUT we see that certification is reasonable using the proposed methodology
www.DLR.de • Chart 25 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Checked and confirmed properties of the model
Model Implementation
Requirements
Formalization
Model CheckingSpecification / Properties
Specification / Properties
valid
www.DLR.de • Chart 26 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Checked and confirmed properties of the system?
Specification / Properties
valid
Model Implementation
Requirements
Formalization
Model Checking
?=
?
?Specification /
Propertiesvalid
Specification / Properties
www.DLR.de • Chart 27 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Checked and confirmed properties of the system!
Model Implementation
Requirements
Formalization
Model Checking
!=
Specification / Properties
Specification / Properties
valid
Runtime Monitoring
Specification / Properties
valid
www.DLR.de • Chart 28 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Runtime Monitor
• A Monitor observes System behavior • Is the system observed behavior consistent to the specification?
• Issued a warning to the user • Initiate an action to ensure a safe system state
• The system under observation can be a program, Hardware, network or any kind of system combination
Monitor
Specification / Properties
Hardware
Software
System
User / Environment
www.DLR.de • Chart 29 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Motivation
• Are the same properties valid for the system as for the model
• Ensuring a safe operation by monitoring of
• Operation specific risk
• Violation of safety requirements
• Functional consistency
• Increase of Situational Awareness
• Control of functional states not available via pilot instruments
www.DLR.de • Chart 30 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Extendable and Scalable Approach
• “Inverse”, safety view on the system functionality • Debugging • Certification Credit • Formal test case • Instant Reaction / Notification • Contingency / Safe Termination • Reduce Software Safety Level • Fail-Safe / Robust Systems
Offline Online Mitigation Runtime Certification
Fail-Safeness
www.DLR.de • Chart 31 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Specific Operation Category Safety Concept
Functional requirements
Safety Assessment
Safety critical system design
Runtime Monitoring
System
Safe Flight Termination
Flight control architecture suitable for runtime monitoring
Monitoring Specification
• Not an “Aircraft Level Authorization”, instead Aircraft + Operation • Analysis of relevant safety requirements • Flight control system architecture with runtime monitoring
specifically to support specific category safety case
www.DLR.de • Chart 32 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Safety-Critical System Architecture
www.DLR.de • Chart 33 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Runtime Monitoring using Temporal Logic (LTL) and Formal Methods
• Research Tool University Saarbrücken: Lola
• Specification language for offline and online monitoring
• Based on mathematical foundation of linear temporal logic
• Lola is based on typed streams, which are used both for the inputs to the monitor as well as for output
• Goal: generate independent standalone executable monitoring module in software or in hardware
Example Lola specification to supervise the allowed flight altitude
www.DLR.de • Chart 34 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Summary
1. Approach based on Formal Methods
• Demonstration based on DLR‘s flight tested unmanned aircraft
guidance software (MiPlEx)
• Qualification for Certification
• Assurance Considerations w.r.t. Autonomy
2. Approach enhancement for new DLR unmanned air freight project
• V&V effort reduction: Explotation of new EASA concept (esp. SORA)
• Technical concept based on Formal Methods
and Runtime Monitoring
www.DLR.de • Chart 35 > DGLR 2016 > Christoph Torens • DGLR Workshop 2016 – Software Safety
Q&A: V&V => christoph.torens@dlr.de MiPlEx => florian.adolf@dlr.de
Requirements
Formalization
Modelling
Model-checking
Certification
Vielen Dank für die
Aufmerksamkeit!
Functional requirements
Safety Assessment
Safety critical system design
Runtime Monitoring
System
Safe Flight Termination