Static detection of implementation errors using formal code specification

Iman Saleh, Gregory Kulczycki, M. Brian Blake, Yi Wei

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80% of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages197-211
Number of pages15
Volume8137 LNCS
DOIs
StatePublished - Oct 24 2013
Externally publishedYes
Event11th International Conference on Software Engineering and Formal Methods, SEFM 2013 - Madrid, Spain
Duration: Sep 25 2013Sep 27 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8137 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other11th International Conference on Software Engineering and Formal Methods, SEFM 2013
CountrySpain
CityMadrid
Period9/25/139/27/13

Fingerprint

Codes (standards)
Specification
Specifications
Formal methods
Formal Specification
Formal Methods
Fault Injection
Algorithms and Data Structures
Software Engineering
Experimentation
Data structures
Software engineering
Quantify
Programming
Partial
Software

Keywords

  • Experimentation
  • Formal Methods
  • Mutation Testing

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Saleh, I., Kulczycki, G., Blake, M. B., & Wei, Y. (2013). Static detection of implementation errors using formal code specification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8137 LNCS, pp. 197-211). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8137 LNCS). https://doi.org/10.1007/978-3-642-40561-7_14

Static detection of implementation errors using formal code specification. / Saleh, Iman; Kulczycki, Gregory; Blake, M. Brian; Wei, Yi.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8137 LNCS 2013. p. 197-211 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8137 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Saleh, I, Kulczycki, G, Blake, MB & Wei, Y 2013, Static detection of implementation errors using formal code specification. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 8137 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8137 LNCS, pp. 197-211, 11th International Conference on Software Engineering and Formal Methods, SEFM 2013, Madrid, Spain, 9/25/13. https://doi.org/10.1007/978-3-642-40561-7_14
Saleh I, Kulczycki G, Blake MB, Wei Y. Static detection of implementation errors using formal code specification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8137 LNCS. 2013. p. 197-211. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-40561-7_14
Saleh, Iman ; Kulczycki, Gregory ; Blake, M. Brian ; Wei, Yi. / Static detection of implementation errors using formal code specification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8137 LNCS 2013. pp. 197-211 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{8789bef7ec774b42933ad63153d99e64,
title = "Static detection of implementation errors using formal code specification",
abstract = "The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80{\%} of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.",
keywords = "Experimentation, Formal Methods, Mutation Testing",
author = "Iman Saleh and Gregory Kulczycki and Blake, {M. Brian} and Yi Wei",
year = "2013",
month = "10",
day = "24",
doi = "10.1007/978-3-642-40561-7_14",
language = "English",
isbn = "9783642405600",
volume = "8137 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "197--211",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Static detection of implementation errors using formal code specification

AU - Saleh, Iman

AU - Kulczycki, Gregory

AU - Blake, M. Brian

AU - Wei, Yi

PY - 2013/10/24

Y1 - 2013/10/24

N2 - The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80% of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.

AB - The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80% of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.

KW - Experimentation

KW - Formal Methods

KW - Mutation Testing

UR - http://www.scopus.com/inward/record.url?scp=84885936369&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84885936369&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-40561-7_14

DO - 10.1007/978-3-642-40561-7_14

M3 - Conference contribution

AN - SCOPUS:84885936369

SN - 9783642405600

VL - 8137 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 197

EP - 211

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -