More Web Proxy on the site http://driver.im/

research-article

Formal specifications better than function points for code sizing

Authors:

Rafal Kolanski,

June Andronick,

Len BassAuthors Info & Claims

ICSE '13: Proceedings of the 2013 International Conference on Software Engineering

Pages 1257 - 1260

Published: 18 May 2013 Publication History

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.

References

[1]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: Formal verification of an OS kernel,” in Proc. of 22nd SOSP. ACM, 2009, pp. 207–220.

Digital Library

[2]

J. Andronick, R. Jeffery, G. Klein, R. Kolanski, M. Staples, H. J. Zhang, and L. Zhu, “Large-scale formal verification in practice: A process perspective,” in Proc. of 34th ICSE. ACM, 2012, pp. 1002–1011.

Digital Library

[3]

J. P. Bowen and M. G. Hinchey, “Ten commandments of formal methods,” Computer, vol. 28, pp. 56–63, 1995.

Digital Library

[4]

S. Gerhart, D. Craigen, and T. Ralston, “Observations on industrial practice using formal methods,” in Proc. of 15th ICSE. IEEE, 1993, pp. 24–33.

Digital Library

[5]

J. P. Bowen and M. G. Hinchey, “Seven more myths of formal methods,” IEEE Software, vol. 12, pp. 34–41, Jul. 1995.

Digital Library

[6]

ISO/IEC 19761:2011, Software engineering — COSMIC: a functional size measurement method, 2011.

[7]

J. Liedtke, “Toward real microkernels,” Communications of the ACM, vol. 39, pp. 70–77, Sep. 1996.

Digital Library

[8]

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002.

Digital Library

[9]

H. J. Zhang, G. Klein, M. Staples, J. Andronick, L. Zhu, and R. Kolanski, “Simulation modeling of a large scale formal verification process,” in Proc. of ICSSP. IEEE, 2012, p. 10.

[10]

The COSMIC Functional Size Measurement Method Version 3.0.1: Measurement Manual, The COSMIC Consortium, May 2009.

[11]

C. Gencel and O. Demirors, “Functional size measurement revisited,” ACM Transactions on Software Engineering and Methodology, vol. 17, pp. 15.1–15.36, 2008.

Digital Library

[12]

J.-M. Desharnais, A. Abran, P. E. Dikici, M. C. Ilis, and I. N. Karaca, “Functional size of a real-time system,” in Proc. of IWSM 2009/Mensura 2009. Springer, 2009, pp. 122–129.

Digital Library

[13]

C. Gencel, R. Heldal, and K. Lind, “On the relationship between different size measures in the software lifecycle,” in Proc. of 16th APSEC. IEEE Computer Society, 2009, pp. 19–26.

Digital Library

[14]

Trustworthy Systems Team, seL4 Reference Manual: API version 1.1, NICTA, 2011.

[15]

J. Rosenberg, “Some misconceptions about lines of code,” in Proc. of 4th METRICS. IEEE, 1997, pp. 137–142.

Digital Library

[16]

ISO/IEC 14143.5:2004, Functional size measurement, Part 5: Determination of functional domains for use with functional size measurement, 2004.

[17]

L. Lavazza and C. Garavaglia, “Using function points to measure and estimate real-time and embedded software: Experiences and guidelines,” in Proc. of 3rd ESEM, 2009, pp. 100–110.

Digital Library

[18]

K. Lind and R. Heldal, “Categorization of real-time software components for code size estimation,” in Proc. of 4th ESEM, 2010.

Digital Library

[19]

O. O. Top, O. Demirors, and B. Ozcan, “Reliability of COSMIC functional size measurement results: A multiple case study on industry cases,” in Proc. of 35th SEAA, 2009, pp. 327–334.

Digital Library

[20]

M. Olszewska and K. Sere, “Specification metrics for Event-B,” in Proc. of 13th CONQUEST, 2010, pp. 20–22.

[21]

T. E. Hastings and A. S. M. Sajeev, “A vector-based approach to software size measurement and effort estimation,” IEEE Transactions on Software Engineering, vol. 27, pp. 337–350, 2001.

Digital Library

[22]

T. Miyawaki, J. Iijima, and S. Ho, “Measuring function points from VDM-SL specifications,” in Proc. of 5th ICSSSM. IEEE, 2008.

[23]

H. Diab, M. Frappier, and R. St-Denis, “A formal definition of function points for automated measurement of B specifications,” in Proc. of 4th ICFEM. Springer, 2002.

Digital Library

Cited By

Matichuk DMurray TAndronick JJeffery RKlein GStaples MBertolino ACanfora GElbaum S(2015)Empirical study towards a leading indicator for cost of formal software verificationProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818842(722-732)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818842
Staples MJeffery RAndronick JMurray TKlein GKolanski RMorisio MDybå TTorchiano M(2014)Productivity for proof engineeringProceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement10.1145/2652524.2652551(1-4)Online publication date: 18-Sep-2014
https://dl.acm.org/doi/10.1145/2652524.2652551

Index Terms

Formal specifications better than function points for code sizing
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
      2. Software implementation planning
        Software design techniques
    2. Software development process management
  2. Software notations and tools

Recommendations

Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies

Creating a formal specification for a design is an error-prone process. At the same time, debugging incorrect specifications is difficult and time consuming. In this work, we propose a debugging method for formal specifications that does not require an ...
Structured formal specifications
Generating Maude formal specifications from AUML diagrams
Selected papers from the International Conference on Computer Science, Software Engineering, Information Technology, e-Business, and Applications, 2004

In this paper, we present a formal and systematic approach allowing translating the specification of the interactions between agents, described using AUML formalism, in a Maude specification. Based on rewriting logic, the formal and object-oriented ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '13: Proceedings of the 2013 International Conference on Software Engineering

May 2013

1561 pages

ISBN:9781467330763

General Chair:
David Notkin,
Program Chairs:
Betty H. C. Cheng,
Klaus Pohl

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

IEEE Press

Publication History

Published: 18 May 2013

Check for updates

Qualifiers

Research-article

Conference

ICSE '13

Sponsor:

SIGSOFT

ICSE '13: 35th International Conference on Software Engineering

May 18 - 26, 2013

CA, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
162
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Matichuk DMurray TAndronick JJeffery RKlein GStaples MBertolino ACanfora GElbaum S(2015)Empirical study towards a leading indicator for cost of formal software verificationProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818842(722-732)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818842
Staples MJeffery RAndronick JMurray TKlein GKolanski RMorisio MDybå TTorchiano M(2014)Productivity for proof engineeringProceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement10.1145/2652524.2652551(1-4)Online publication date: 18-Sep-2014
https://dl.acm.org/doi/10.1145/2652524.2652551

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten