Skip to main content


Formal specifications better than function points for code sizing


Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass




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.

BibTeX Entry

    publisher        = {IEEE},
    author           = {Staples, Mark and Kolanski, Rafal and Klein, Gerwin and Lewis, Corey and Andronick, June and Murray,
                        Toby and Jeffery, Ross and Bass, Len},
    month            = may,
    editor           = {{David Notkin, Betty H. C. Cheng, Klaus Pohl}},
    year             = {2013},
    title            = {Formal Specifications Better Than Function Points for Code Sizing},
    booktitle        = {International Conference on Software Engineering},
    pages            = {1257-1260},
    address          = {San Francisco, USA}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.