Name
Abstract | ||
|---|---|---|
Size and effort estimation is a significant challenge for the management of large-scale formal verification projects. We report on an initial study of relationships between the sizes of artefacts from the development of seL4, a formally-verified embedded systems microkernel. For each API function we first determined its COSMIC Function Point (CFP) count (based on the seL4 user manual), then sliced the formal specifications and source code, and performed a normalised line count on these artefact slices. We found strong and significant relationships between the sizes of the artefact slices, but no significant relationships between them and the CFP counts. Our finding that CFP is poorly correlated with lines of code is based on just one system, but is largely consistent with prior literature. We find CFP is also poorly correlated with the size of formal specifications. Nonetheless, lines of formal specification correlate with lines of source code, and this may provide a basis for size prediction in future formal verification projects. In future work we will investigate proof sizing.
|
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/ICSE.2013.6606692 | ICSE |
Keywords | Field | DocType |
application program interfaces,embedded systems,formal specification,operating system kernels,program slicing,program verification,software development management,API function,COSMIC Function Point,code sizing,formal specifications,formally-verified embedded systems microkernel,large-scale formal verification projects,seL4,source code | Program slicing,Programming language,Source code,Computer science,Microkernel,Function point,Real-time computing,Formal specification,Formal methods,Formal verification,Source lines of code | Conference |
Volume | ISBN | Citations |
2 | 978-1-4673-3076-3 | 5 |
PageRank | References | Authors |
0.44 | 14 | 8 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mark Staples | 1 | 515 | 38.02 |
| Rafal Kolanski | 2 | 802 | 34.23 |
| Gerwin Klein | 3 | 1450 | 87.47 |
| Corey Lewis | 4 | 33 | 3.30 |
| June Andronick | 5 | 903 | 42.66 |
| Toby Murray | 6 | 242 | 17.03 |
| D. Ross Jeffery | 7 | 753 | 63.72 |
| Len Bass | 8 | 1501 | 162.21 |