Systems Verification: Difference between revisions
Jump to navigation
Jump to search
mNo edit summary |
|||
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
Current Participants: | Current Participants: | ||
*[http://www.cs.caltech.edu/cspeople/faculty/chandy_m.html K. Mani Chandy] (Professor, CS) | *[http://www.cs.caltech.edu/cspeople/faculty/chandy_m.html K. Mani Chandy] (Professor, CS) | ||
*[http://www.cds.caltech.edu/people/portal/?id=758 Vanessa D. Jönsson] (Student, CDS) | |||
*[http://www.cds.caltech.edu/~andyl/ Andrew Lamperski] (Student, CDS) | *[http://www.cds.caltech.edu/~andyl/ Andrew Lamperski] (Student, CDS) | ||
*[http://www.ist.caltech.edu/~mitras/ Sayan Mitra] (Postdoc, CS) | *[http://www.ist.caltech.edu/~mitras/ Sayan Mitra] (Postdoc, CS) | ||
*[http://www.cds.caltech.edu/~dtarraf/ Danielle C.Tarraf] (Assistant Professor, Johns Hopkins) | *[http://www.cds.caltech.edu/~dtarraf/ Danielle C.Tarraf] (Assistant Professor, Johns Hopkins) | ||
<br/> | |||
To subscribe to the mailing list: | |||
[http://listserv.cds.caltech.edu/mailman/listinfo/verification verification AT cds dot caltech dot edu ] | |||
<br/> | |||
== Upcoming Events == | |||
[[Caltech Verification Workshop 2009]] | |||
July 7 – 14, 2008, 20th International Conference on Computer Aided Verification, Princeton, USA [http://www.princeton.edu/cav2008/ CAV 2008] | July 7 – 14, 2008, 20th International Conference on Computer Aided Verification, Princeton, USA [http://www.princeton.edu/cav2008/ CAV 2008] | ||
| Line 14: | Line 21: | ||
This research effort focuses on bridging theoretical frameworks related to systems verification applied to different fields such as software, controls and biology. These systems can be modeled as discrete, continuous or hybrid dynamical systems with added performance specifications, some of which include safety constraints, stability or the existence of a recurring state. Techniques for verifying a given system's adherence to design specifications vary from field to field. Our goal is to provide a theoretical foundation for verification that is adaptable to different domains. | This research effort focuses on bridging theoretical frameworks related to systems verification applied to different fields such as software, controls and biology. These systems can be modeled as discrete, continuous or hybrid dynamical systems with added performance specifications, some of which include safety constraints, stability or the existence of a recurring state. Techniques for verifying a given system's adherence to design specifications vary from field to field. Our goal is to provide a theoretical foundation for verification that is adaptable to different domains. | ||
Currently, we are concentrating our efforts on relating techniques in robust control design to software verification concerns. | Currently, we are concentrating our efforts on relating techniques in robust control design to software verification concerns. | ||
== Publications == | == Publications == | ||
| Line 26: | Line 34: | ||
==== Verification and Control ==== | ==== Verification and Control ==== | ||
* D. C. Tarraf, A. Megretski and M. A. Dahleh, A Framework for Robust Stability of Systems Over Finite Alphabets, To appear in IEEE Transactions on Automatic Control, June 2008. | * D. C. Tarraf, A. Megretski and M. A. Dahleh, <i>A Framework for Robust Stability of Systems Over Finite Alphabets</i>, To appear in IEEE Transactions on Automatic Control, June 2008. | ||
* E. Klavins, R. Ghrist, and D. Lipsky, Graph Grammars for Self-Assembling Robotic Systems, Proceedings of the International Conference on Robotics and Automation. May, 2004, pp. 5293- 5300 [http://faculty.washington.edu/klavins/papers/icra04-sa.pdf pdf] | * E. Klavins, R. Ghrist, and D. Lipsky, <i>Graph Grammars for Self-Assembling Robotic Systems</i>, Proceedings of the International Conference on Robotics and Automation. May, 2004, pp. 5293- 5300 [http://faculty.washington.edu/klavins/papers/icra04-sa.pdf pdf] | ||
* Delvenue, Blondel, Complexity of Control On Finite Automata, [http://www.inma.ucl.ac.be/%7Eblondel/publications/05DB-controlauto.pdf pdf] | * Delvenue, Blondel,<i> Complexity of Control On Finite Automata</i>, [http://www.inma.ucl.ac.be/%7Eblondel/publications/05DB-controlauto.pdf pdf] | ||
==== Model Checking on Cellular Automata ==== | ==== Model Checking on Cellular Automata ==== | ||
* K.Sutner, Model Checking One-Dimensional Cellular Automata, Submitted JCA. [http://www.cs.cmu.edu/~sutner/papers/auto07-jca.pdf pdf] | * K.Sutner, <i>Model Checking One-Dimensional Cellular Automata</i>, Submitted JCA. [http://www.cs.cmu.edu/~sutner/papers/auto07-jca.pdf pdf] | ||
* M. D'Antonio, G. Delzanno, SAT-based analysis of cellular automata, Lecture Notes in Computer Science, Volume 3305/2004, 2004. [http://www.cs.unipr.it/CILC04/DownloadArea/DAntonioD-CILC04.pdf pdf] | * M. D'Antonio, G. Delzanno, <i>SAT-based analysis of cellular automata</i>, Lecture Notes in Computer Science, Volume 3305/2004, 2004. [http://www.cs.unipr.it/CILC04/DownloadArea/DAntonioD-CILC04.pdf pdf] | ||
==== General References ==== | |||
* E. Clarke, O. Grumberg, D. A. Peled, <i> Model Checking </i>, [http://www.amazon.com/Model-Checking-Edmund-Clarke-Jr/dp/0262032708/ref=sr_1_1?ie=UTF8&s=books&qid=1212092439&sr=8-1 ref] | |||
* C. Baier, J. Katoen, <i>Principles of Model Checking</i> [http://www.amazon.com/Principles-Model-Checking-Representation-Mind/dp/026202649X/ref=sr_1_2?ie=UTF8&s=books&qid=1212092660&sr=1-2 ref] | |||
Latest revision as of 19:32, 30 January 2009
Current Participants:
- K. Mani Chandy (Professor, CS)
- Vanessa D. Jönsson (Student, CDS)
- Andrew Lamperski (Student, CDS)
- Sayan Mitra (Postdoc, CS)
- Danielle C.Tarraf (Assistant Professor, Johns Hopkins)
To subscribe to the mailing list:
verification AT cds dot caltech dot edu
Upcoming Events
Caltech Verification Workshop 2009
July 7 – 14, 2008, 20th International Conference on Computer Aided Verification, Princeton, USA CAV 2008
Objectives
This research effort focuses on bridging theoretical frameworks related to systems verification applied to different fields such as software, controls and biology. These systems can be modeled as discrete, continuous or hybrid dynamical systems with added performance specifications, some of which include safety constraints, stability or the existence of a recurring state. Techniques for verifying a given system's adherence to design specifications vary from field to field. Our goal is to provide a theoretical foundation for verification that is adaptable to different domains. Currently, we are concentrating our efforts on relating techniques in robust control design to software verification concerns.
Publications
Lectures
"Model Checking with Automata"
Related Reading
Verification and Control
- D. C. Tarraf, A. Megretski and M. A. Dahleh, A Framework for Robust Stability of Systems Over Finite Alphabets, To appear in IEEE Transactions on Automatic Control, June 2008.
- E. Klavins, R. Ghrist, and D. Lipsky, Graph Grammars for Self-Assembling Robotic Systems, Proceedings of the International Conference on Robotics and Automation. May, 2004, pp. 5293- 5300 pdf
- Delvenue, Blondel, Complexity of Control On Finite Automata, pdf
Model Checking on Cellular Automata
- K.Sutner, Model Checking One-Dimensional Cellular Automata, Submitted JCA. pdf
- M. D'Antonio, G. Delzanno, SAT-based analysis of cellular automata, Lecture Notes in Computer Science, Volume 3305/2004, 2004. pdf