Caltech Workshop on Verification and Validation
 |
| Caltech Workshop on Verification and Validation |
| 23-24 September 2009 Pasadena, CA |
Description
Formal verification and validation (V&V) have been subject to research in controls, computer science, and networking but often in isolation from each other. With recent convergence of controls, computation, and communication, there is a need for unified theories and algorithms. Despite advances in V&V tools in respective areas, such unification is in its infancy. Moreover, rigorous V&V for systems of current interest is a complicated task due to common difficulties including the interaction between the software and the physical world, untraditional information flow, modeling/environmental uncertainties, and unavoidable explosion of computational complexity of the currently available tools (in both domains).
We believe that the success of formal methods and V&V in the intersection of controls, computer science, and networking is stringent on the development truly hybrid methods that blend ideas from all these areas and possibly others. The main purpose of the proposed workshop is to bring experts from academia, industry, and governmental agencies together and promote exchange of ideas and establishment of interdisciplinary collaborations. We will emphasize the integration of the tools and ideas from these fields to lead to a unified toolset. Moreover, we are expecting to highlight current trends and future directions in V&V research as well as industrial needs and requirements for V&V through outlook sessions and talks by experts from the industry and government agencies.
Schedule
September 23, 2009
- 8:00 - 8:30 - Registration and breakfast
- 8:30 - Opening remarks
- 8:45 - Karl-Erik Arzen "On verification and validation of real-time control systems: formal approaches vs simulation"
- 9:15 - Gerard Holzmann "The practice of formal methods"
- 9:45 - Brian Williams "Managing risk and uncertainty in model-based programs"
- 10:15 - Break
- 10:45 - Mani Chandy "New models and theory for game theory with message passing"
- 11:15 - Nancy Leveson "A new control theoretic foundation for safety engineering"
- 11:45 - Lunch
- 1:15 - Rupak Majumdar "Symbolic robustness analysis"
- 1:45 - Paulo Tabuada "From formal verification to formal synthesis"
- 2:15 - Break
- 2:45 - Sayan Mitra "Replication-based fault-tolerance of wireless distributed control systems"
- 3:15 - Stavros Tripakis "Implementation of synchronous programs on asynchronous execution platforms: correctness, modularity, and performance analysis"
- 3:45 - Break
- 4:00-5:00 - Panel (Successful applications and current status; bridging communities) - Rajeev Alur, Mani Chandy (moderator), Gerard Holzmann, Stephen Jacklin, Gabor Karsai
September 24, 2009
- 8:00 - 8:30 - Breakfast
- 8:30 - Edmund Clarke "Model checking: making it scale"
- 9:00 - Eric Feron "Control systems software assurance"
- 9:30 - Rajeev Alur "Interfaces for control components"
- 10:00 - Allessandro Pinto "Formal verification and analytical methods for complex systems: The UTRC experience"
- 10:30 - Break
- 11:00-12:00 - Panel (Challenges and future research directions) - Andrzej Banaszuk, Devesh Bhatt, Michael Branicky, Ken Butts, John Doyle (moderator), Douglas Stuart
- 12:00 - Lunch
- 1:30 - Andrew Packard - "Quantitative local analysis for continuous nonlinear systems"
- 2:00 - Ashish Tiwari "Verification using constraint solving"
- 2:30 - Domitilla Del Vecchio "Dynamic feedback for hybrid systems on a partial order"
- 3:00 - Break
- 3:30 - Calin Belta "Formal approaches to robot motion planning and control"
- 4:00 - Koushik Sen "Testing concurrent programs"
- 4:30 - Andre Platzer "Hybrid logical verification for hybrid systems"
Workshop Venue
Room 105 in the Annenberg Building
Annenberg Building is a new building on the Caltech campus and is not on the campus maps. A campus map with the rough location of the building marked is here.
Local transportation and parking on campus
A shuttle service between the Sheraton Hotel and the Caltech campus will be available. Information will be posted on this page a few days before the workshop.
Information for parking on campus.
Hotel and Travel
A block of rooms have been reserved at The Sheraton Pasadena Hotel for the nights of September 22-24:
303 East Cordova Street, Pasadena, CA 91101
Phone: (626) 449-4000
Reservation information
- Reservations are to be made by the individual calling the hotel directly at (626) 449-4000 or 1-800-457-7940 and asking for the Reservations Department. Please use the group rate for the Caltech Workshop on Verification and Validation.
- If you cannot make the call to the hotel, please inform us for assistance.
- The cut-off date for the availability of this block of rooms is September 1st. Please try to reserve your rooms before this date or let us know for extensions.
Getting to Caltech
LAX to Caltech
Take Sepulveda Blvd. to the Glen Anderson Fwy (105) east to the Harbor Fwy (110) north to the Pasadena Fwy, which becomes the Arroyo Parkway. Take the Arroyo Parkway straight ahead (north); turn right (east) on Del Mar Blvd. Turn right onto Holliston and park in the lot. Parking permits are available on the third level (follow the signs).
Shuttle van services from/to LAX
Burbank Airport to Caltech
Take the Golden State Fwy (Interstate 5) south to the Ventura Fwy (134) east to the Foothill Fwy (210) east. Exit Hill Avenue; turn right (south) onto Hill. Take Hill south to Del Mar Blvd.; turn right (west) onto Del Mar. Turn left onto Holliston (first street) and park in the lot. Parking permits are available on the third level (follow the signs).
Local transportation from/to Burbank Airport (click on Transportation in the left menu)
Organizers
- Mani Chandy (Caltech, CS)
- Richard Murray (Caltech, CDS)
- Paulo Tabuada (UCLA, ECE)
- Ufuk Topcu (Caltech, CDS)
The Caltech Verification and Validation Workshop, 2009 is sponsored by Caltech's Center for the Mathematics of Information and the Air Force Office of Scientific Research (through the MURI "Specification, Design and Verification of Distributed Embedded Systems").
