Formal Specification and Verification

Purpose

Developing tools and methodology for the formal specification and verification of network protocols. We attempt to use existing tools and develop newer formalisms and tools where necessary.

People

Tools

Status

  • Developed a Reference Model for software development. Demonstrated its use for a network benchmark called the Village Telephone System
  • Attempted to define a language for specifying protocols called Protocol Object Pseudo Code (POPC)
  • Ongoing effort to integrate the HOL90 theorem prover with the SPIN model checker
    •

    Papers

    [1] Davor Obradovic and Elsa Gunter. Towards the Integration of Model Checking and Theorem Proving: Embedding a Subset of Promela into HOL, Category B paper, Theorem Proving and Higher Order Logics, August 2000.
    BibTeX entry. Download PS.
    [2] Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, and Pamela Zave. The Village Telephone System: A case study in formal software engineering. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics 11th International Conference TPHOLs '98, volume 1479 of Lecture Notes in Computer Science, pages 49-66, Canberra, Australia, September 1998. Springer.
    BibTeX entry. Download PS.
    [3] Carl A. Gunter, Elsa L. Gunter, Michael Jackson, and Pamela Zave. A reference model for requirements and specifications (abstract), June 2000. Best Paper for International Conference on Requirements Engineering.
    BibTeX entry. Download PS.