Conference Proceedings
Formal specifications better than function points for code sizing
M Staples, R Kolanski, G Klein, C Lewis, J Andronick, T Murray, R Jeffery, L Bass
Proceedings of the 35th International Conference on Software Engineering | Association for Computing Machinery | Published : 2013
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 correla..
View full abstractGrants
Funding Acknowledgements
NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.