Design and Verification of Autonomous System Controllers
Design And Verification of Autonomous
System
Controllers Under Timing Uncertainties
Bineet Ghosh
1
Quantitative Safety: Robot Maneuvers
2
Robot trying to reach its destination, avoiding obstacles.
Obstacles
Nominal Trajectory:
Planned Path
Implementing Controllers
3
The robot is running multiple jobs on its processor!
Heat Control
Perception
Path Follower
Multiple
Jobs
All jobs cannot always be scheduled—deadline misses!
Responsible for moving the robot along
the planned trajectory.
What if the path follower misses its deadline?
Quantitative Safety: Robot Maneuvers
4
What if the path follower misses some deadlines?
The trajectory can
deviate from the
nominal trajectory!
Quantitative Safety: Robot Maneuvers
5
What if the path follower misses some deadlines?
The trajectory can
deviate from the
nominal trajectory!
Trajectory
under deadline
misses
Quantitative Safety: Robot Maneuvers
6
What if the path follower misses
more
deadlines?
The trajectory can deviate
more
from the nominal
trajectory!
Quantitative Safety: Robot Maneuvers
7
What if the path follower misses
more
deadlines?
The trajectory can deviate
more
from the nominal
trajectory!
And become unsafe!
Quantitative Safety: Robot Maneuvers
8
In Conclusion: Not all
patterns
of deadline misses are
safe
!
Goal:
Detect if a
given
pattern
of
deadline misses is
safe!
Quantitative Safety: Robot Maneuvers
9
Achieve that by….
Maximum
Deviation
Compute
Goal
Computing Deviation: A Naïve Approach
10
•
Given a pattern of deadline misses.
0: Deadline Miss.
1: Deadline Hit (No Miss).
11
•
Given a pattern of deadline misses.
•
Instead:
Compute an over-approximation of the maximum deviation.
Computing Deviation: A Naïve Approach
•
Requires computing
reachable sets
.
•
Disadvantages:
•
Computationally slower (generally).
•
The computed bounds on the maximum deviation are not tight (generally).
12
Computing Deviation: Other Approaches
C. Hobbs,
B. Ghosh
, et al., "Safety Analysis of Embedded Controllers under Implementation Platform Timing Uncertainties," in IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022.
What I Propose…
•
Compute an
upper bound
of the
maximum deviation
under a
pattern
of deadline misses
.
•
Statistical Approach:
guarantees are probabilistic.
•
Advantages
:
•
Computationally faster than non-probabilistic approaches.
•
Tighter bounds on the computed maximum deviation.
13
B. Ghosh
et al., "Statistical Hypothesis Testing of Controller Implementations Under Timing Uncertainties," 2022 IEEE 28th International
Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA).
Best Paper Candidate.
Approach Overview
14
System Model, Initial State
Small number of
random runs
Hypothesis Test
Initial
guess
Yes
Counter
example
No
Hypothesizer
Verifier
Refiner
Refined
Input
Guess the
deviation!
Verify the
guessed
deviation!
Refine the
deviation
Keep refining
and verifying!
Once verified
successfully!
Computed upper
bound on deviation
Designing Schedulers
15
This approach can be further used to design schedulers!
Heat Control
Perception
Path Follower
Schedule
s.t.
none of the
processes violate safety!
Designing Schedulers
16
We propose the following…
Heat Control
Perception
Path Follower
S. Xu,
B. Ghosh
, et al., "Safety-aware Flexible
Schedule Synthesis for Cyber-Physical Systems using
Weakly-Hard Constraints," in
Asia and South Pacific
Design Automation Conference
, 2022.
Using the Proposed Approach
Safe Behavior For All The Processes
Construct an
Automaton
Conclusion
•
Statistical approach to compute maximum deviation under
deadline misses!
•
My approach computes tighter upper bounds with less computation time.
•
Further, using this approach, we can construct schedules that do not
violate safety
•
Future Work:
Complicated deadline miss patterns, and more general
schedules.
17
The open-source prototype tool,
StatDev
, is available at:
github.com/bineet-
coderep/StatJitteryScheduler
Thank You!
Thank You!
37
Scan this QR
code on your
phone
• Hello everyone, I am Bineet Ghosh. A PhD Student from The University of North Carolina at Chapel Hill.
• My research focuses on Designing and Verification of Autonomous Systems.
• Today, I am going to talk about an approach to design and verify autonomous system controllers, under the presence of timing uncertainties.
Explore the challenges of designing autonomous system controllers under timing uncertainties, focusing on quantitative safety measures to ensure the robot maneuvers safely despite deadline misses. The study delves into implementing controllers, analyzing trajectory deviations under different scenarios of deadline misses, and aims to detect safe patterns of operation. Various strategies for achieving quantitative safety in robot maneuvers are discussed, emphasizing the importance of computing goal maximum deviation.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
1 Design And Verification of Autonomous System Controllers Under Timing Uncertainties Bineet Ghosh bineet@cs.unc.edu cs.unc.edu/~bineet
2 Quantitative Safety: Robot Maneuvers Robot trying to reach its destination, avoiding obstacles. Obstacles Nominal Trajectory: Planned Path
3 Implementing Controllers The robot is running multiple jobs on its processor! Path Follower Responsible for moving the robot along the planned trajectory. Multiple Jobs Perception All jobs cannot always be scheduled deadline misses! Heat Control What if the path follower misses its deadline?
4 Quantitative Safety: Robot Maneuvers What if the path follower misses some deadlines? The trajectory can deviate from the nominal trajectory!
5 Quantitative Safety: Robot Maneuvers What if the path follower misses some deadlines? The trajectory can deviate from the nominal trajectory! Trajectory under deadline misses
6 Quantitative Safety: Robot Maneuvers What if the path follower misses more deadlines? The trajectory can deviate more from the nominal trajectory!
7 Quantitative Safety: Robot Maneuvers What if the path follower misses more deadlines? The trajectory can deviate more from the nominal trajectory! And become unsafe!
8 Quantitative Safety: Robot Maneuvers In Conclusion: Not all patterns of deadline misses are safe! Goal: Detect if a given pattern of deadline misses is safe!
9 Quantitative Safety: Robot Maneuvers Achieve that by . Compute Goal Maximum Deviation
10 Computing Deviation: A Na ve Approach Given a pattern of deadline misses. Compute the maximum deviation up-to a bounded time ?. A Possible Behavior up-to Time ?: 1 1 0 1 1 0 0 1 0/1-sequence of length ? 0: Deadline Miss. 1: Deadline Hit (No Miss).
11 Computing Deviation: A Na ve Approach Given a pattern of deadline misses. Compute the maximum deviation up-to a bounded time ?. Na ve Approach: Requires computing deviation of 2? many trajectories! Instead: Compute an over-approximation of the maximum deviation.
12 Computing Deviation: Other Approaches Requires computing reachable sets. Disadvantages: Computationally slower (generally). The computed bounds on the maximum deviation are not tight (generally). C. Hobbs, B. Ghosh, et al., "Safety Analysis of Embedded Controllers under Implementation Platform Timing Uncertainties," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022.
13 What I Propose Compute an upper bound of the maximum deviation under a pattern of deadline misses. Statistical Approach: guarantees are probabilistic. Advantages: Computationally faster than non-probabilistic approaches. Tighter bounds on the computed maximum deviation. B. Ghosh et al., "Statistical Hypothesis Testing of Controller Implementations Under Timing Uncertainties," 2022 IEEE 28th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA). Best Paper Candidate.
14 Keep refining and verifying! Approach Overview Input System Model, Initial State Verifier Formulate ?? and ?? with ??? Small number of random runs Guess the deviation! Generate ? random runs Initial guess Once verified successfully! Verify the guessed Compute ??? Hypothesis Test deviation! Hypothesizer Refined Refine the deviation Is ?? accepted ? Refine ??? Refiner ??? Counter example Yes No Computed upper bound on deviation
15 Designing Schedulers This approach can be further used to design schedulers! Path Follower Perception Heat Control Schedule s.t. none of the processes violate safety!
16 Designing Schedulers We propose the following Path Follower Perception Heat Control Using the Proposed Approach Safe Behavior For All The Processes Construct an Automaton S. Xu, B. Ghosh, et al., "Safety-aware Flexible Schedule Synthesis for Cyber-Physical Systems using Weakly-Hard Constraints," in Asia and South Pacific Design Automation Conference, 2022.
17 Conclusion Statistical approach to compute maximum deviation under deadline misses! My approach computes tighter upper bounds with less computation time. Further, using this approach, we can construct schedules that do not violate safety Future Work: Complicated deadline miss patterns, and more general schedules.
37 Scan this QR code on your phone The open-source prototype tool, StatDev, is available at: github.com/bineet- coderep/StatJitteryScheduler Thank You!
