MURI Telecon 2005-07-13

Agenda

Eric

V&V is really messy and hard the way that it is currently done
Experience working with Boeing/OCP isn't encouraging
How do you make code for a distributed system in a straightforward way that is automatically checked, etc?
How do you know the way the controller is switched on/off is worked into the system?
Systems Eric can get his head around are much simpler; agents running a controller, switching based on messages, etc. Can put into formal setting and reason about it; not clear how to reason about the dynamics
Interested in figuring out how to build these sorts of systems using structured principles

John

Focus on basic science - create theoretical infrastructure that addresses all of the research concentration areas
Start with Prajna thesis - V&V of hybrid systems
Build this into the SoS framework (Pablo can elaborate)
Restrict the expressiveness of the languages (protocols, not systems). Restrict the kind of hacks people can do.
Have examples of distributed systems using protocol stacks - use this sort of an architecture
Think about the mathematics

Mani

Doing things bottom up (starting with code that someone has developed) is impossible
Start top down: what's the language for specification (temporal logic, some variant?)
What is the theory behind the specification
SoS + temporal logic
Add Gerard Holzman (JPL), Rajiv Joshi (JPL)?
Specification, theorem proving, etc
Try to stay out of things like CORBA and other large systems that people have built up
Use of probability: can we prove things things in a probabalistic manner?

Pablo

Particularly interested in how we integrate discrete and continuous parts
One possibility is establishing a middle layer where we can assert things about the time evolution (certain things will transition in a period of time)
Barrier work of Steven could be a start; is there a way to integrate things in a tighter way?
Incorporate adversarial effort?
Erik: moving back and forth between writing continuous part using discrete language versus the other way
Common way of thinking about: polynomial representations for discrete problems. But these are extremely structured proofs.

Possible key themes:
- Problem features: hybrid, distributed, stochastic, adversarial
- Fundamental framework for reasoning about distributed computation for real-time, feedback systems
- Top-down approach: think about a language for specifications that we can reason about
- Think about whether we can incorporate probability in a formal way

Homework
- Put together set of 3-5 papers describing the basic ideas that we want to build on
- CCL paper
- V&V from Mani
- SoS Barrier Certificates