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; it 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 parallel as well as iterative work during execution. We examine some possible improvements on the formal verification process in light of the simulation results. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1109/ICSSP.2012.6225979 | ICSSP |
Keywords | Field | DocType |
microkernel,simulation modeling,process optimization,large-scale machine-checked formal verification,process dynamic characteristics,functional correctness,version control data,process planning,operating system kernels,middle-out process,code level,sel4 operating system microkernel,descriptive process model,project history,project logs,complex coupling impact,process simulation,l4.verified project,meeting notes,software development processes,software process modeling,system dynamics,program verification,secure embedded l4 microkernel,formal verification,data models,computer bugs,software development process,kernel,process model,simulation model,operating system,data model,prototypes,process control,version control | Data modeling,Verification and validation of computer simulation models,Software engineering,Systems engineering,Computer science,Correctness,Microkernel,Process simulation,Process control,Software development process,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4673-2350-5 | 4 | 0.46 |
References | Authors | |
10 | 6 |
Name | Order | Citations | PageRank |
---|---|---|---|
He Zhang | 1 | 817 | 65.63 |
Gerwin Klein | 2 | 1450 | 87.47 |
Mark Staples | 3 | 515 | 38.02 |
June Andronick | 4 | 903 | 42.66 |
Liming Zhu | 5 | 195 | 31.59 |
Rafal Kolanski | 6 | 802 | 34.23 |