Trustworthy Systems

Formal specifications better than function points for code sizing

Authors

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

NICTA

UNSW

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.

BibTeX Entry

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

Download