Simulation Modeling of A Large Scale Formal Verification Process

Select |




Print


Zhang, He (Jason); Klein, Gerwin; Staples, Mark; Andronick, June; Zhu, Liming; Kolanski, Rafal

Zhang, He (Jason); Klein, Gerwin; Staples, Mark; Andronick, June; Zhu, Liming; Kolanski, Rafal


2012-06-02


Conference Material


International Conference on Software and Systems Process


Zurich, Switzerland


3-12


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.


IEEE


software process modeling, process simulation, formal verification, system dynamics, microkernel


http://www.icsp-conferences.org/


978-1-4673-2351-2


nicta:5605


Zhang, He (Jason); Klein, Gerwin; Staples, Mark; Andronick, June; Zhu, Liming; Kolanski, Rafal. Simulation Modeling of A Large Scale Formal Verification Process. In: Ross Jeffery, David Raffo, Ove Armbrust, Li Guo Huang Editor, editor/s. International Conference on Software and Systems Process; Zurich, Switzerland. IEEE; 2012-06-02. 3-12.



Loading citation data...

Citation counts
(Requires subscription to view)