Skip to main content

TS

Simulation modeling of a large scale formal verification process

Authors

Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski

NICTA

UNSW

Abstract

The L4.verified project successfully completed a large-scale machine-checked formal verification at the code level of the functional correctness of the seL4 operating system microkernel. The project applied a middle-out process, which is significantly different from conventional software development processes. This paper reports a simulation model of this process, and is the first simulation model of a formal verification process. The model aims to support further understanding and investigation of the dynamic characteristics of the process and to support planning and optimization of future process enactment. We based the simulation model on a descriptive process model and information from project logs, meeting notes, and version control data over the project's history. Simulation results from the initial version of the model show the impact of complex coupling among the activities and artifacts, and frequent work in parallel and iterations during the execution. A few findings for possible improvements on the formal verification process are suggested in light of the results.

BibTeX Entry

  @inproceedings{Zhang_KSAZK_12,
    publisher        = {IEEE},
    isbn             = {978-1-4673-2351-2},
    author           = {Zhang, He (Jason) and Klein, Gerwin and Staples, Mark and Andronick, June and Zhu, Liming and
                        Kolanski, Rafal},
    month            = {jun},
    editor           = {{Ross Jeffery, David Raffo, Ove Armbrust, Li Guo Huang}},
    year             = {2012},
    keywords         = {software process modeling, process simulation, formal verification, system dynamics, microkernel},
    title            = {Simulation Modeling of A Large Scale Formal Verification Process},
    booktitle        = {International Conference on Software and Systems Process},
    pages            = {3-12},
    address          = {Zurich, Switzerland}
  }

Download