search

GaloisInc / csaf

Control Systems Analysis Framework - a framework to minimize the effort required to evaluate, implement, and verify controller design (classical and learning enabled) with respect to the system dynamics.
BSD 3-Clause "New" or "Revised" License
11 stars 4 forks source link

Reachability analysis + CSAF integration #68

Closed podhrmic closed 3 years ago

podhrmic commented 3 years ago

In GitLab by @bauer-matthews on Sep 30, 2020, 07:28

podhrmic commented 3 years ago

In GitLab by @zutshi on Sep 30, 2020, 10:03

changed title from {-Design FlowStar-} + CSAF integration to {+Reachability analysis+} + CSAF integration

podhrmic commented 3 years ago

In GitLab by @zutshi on Sep 30, 2020, 10:04

Renamed it to reachability analysis. Reasons and details follow.

This is a non-trivial and a research task and it is still not clear if we have the budget for a full flow integration. I am going to wait on this till we have a clear go-ahead from @cslockett. Moreover, integration with flow will involve externals who are not obligated to wrap it up. So I won't put that in the release path.

But what I will like to do is to develop our own version of reachability analysis, for which I estimate a range of 80-100hrs to have it up and running and then some more time time to tweak its performance. There is still a risk of poor results.

podhrmic commented 3 years ago

In GitLab by @bauer-matthews on Oct 1, 2020, 04:08

@zutshi Would our custom reachability analysis be based on simulation, or something else?

podhrmic commented 3 years ago

In GitLab by @podhrmic on Oct 1, 2020, 08:43

Just a ballpark number based on the runs that @EthanJamesLewdid - on a modern machine you can run ~1 simulation per second with parallel runners. So 100 hours = 100*3600 = 360000 simulations. Is that a number you are hoping to get?

podhrmic commented 3 years ago

In GitLab by @podhrmic on Oct 1, 2020, 08:45

Updated the milestone since this is not required for Alpha.

podhrmic commented 3 years ago

In GitLab by @zutshi on Oct 3, 2020, 11:53

No, a reach set analysis for proving safety properties can not be simulation based, as simulations are approximate. When talking about proofs, we need soundness and hence a procedure to symbolically analyze the system and over-approximate the reachable states. Common approaches use domains (like abstract interpretation) including intervals, zonotopes, polytopes, support functions, taylor models.

podhrmic commented 3 years ago

In GitLab by @zutshi on Oct 3, 2020, 12:02

In general, this is extremely slow to do reasonable random testing or training deep NNs on a pc (might scale on a cluster) and I can elaborate more on this if people are interested. However, we should probably compare it to some baseline simulator. The low performance is expected as the current version of CSAF is not geared towards performance at all.

podhrmic commented 3 years ago

In GitLab by @podhrmic on Oct 6, 2020, 10:04

If you need to run the simulation/training faster, I can get you remote access to a beefier machine, just let me know.

podhrmic commented 3 years ago

In GitLab by @zutshi on Oct 6, 2020, 22:28

Got it. But, the point I was trying to make was that for CSAF to be useful for simulation heavy use-cases like training ML algorithms and testing, it will need to be optimized for execution.

podhrmic commented 3 years ago

In GitLab by @podhrmic on Jul 13, 2021, 14:19

@zutshi is this still relevant or can we close it?