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

article

A historical perspective on runtime assertion checking in software development

Authors:

Lori A. Clarke,

David S. RosenblumAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 31, Issue 3

Pages 25 - 37

https://doi.org/10.1145/1127878.1127900

Published: 01 May 2006 Publication History

Abstract

This report presents initial results in the area of software testing and analysis produced as part of the Software Engineering Impact Project. The report describes the historical development of runtime assertion checking, including a description of the origins of and significant features associated with assertion checking mechanisms, and initial findings about current industrial use. A future report will provide a more comprehensive assessment of development practice, for which we invite readers of this report to contribute information.

References

[1]

Abrial, J.-R., Schuman, S. A. and Meyer, B. Specification Language. in McKeag, R. M. and MacNaghtam, A. M. eds. On the Construction of Programs, Cambridge University Press, New York, 1980, 343--410.

[2]

Allers, J. A., Huizinga, A. H., Kukla, J. A., Sipes, J. D. and Yeh, R. T., No. 5 ESS-strategies for Reliability in a Distributed Processing Environment. in 13th International Symposium on Fault-Tolerant Computing, (Milan, Italy, 1983), 388--391.

[3]

ALRM83. Reference Manual for the Ada Programming Language, United States Department of Defense, Washington DC, 1983.

[4]

Ambler, A. L., Good, D. I., Browne, J. C., Burger, W. F., Cohen, R. M., Hoch, C. G. and Wells, R. E., Gypsy: A Language for Specification and Implementation of Verifiable Programs. in ACM Conference on Language Design for Reliable Software, (Raleigh, North Carolina, 1977), 1--10.

Digital Library

[5]

Amey, P. and Chapman, R., Industrial Strength Exception Freedom. in Proceedings of the ACM SIGAda International Conference on Ada, (Houston, Texas, 2002), ACM, 1--9.

Digital Library

[6]

Archer, T. and Whitechapel, A. Inside C#. Microsoft Press, Redmond, WA, 2002.

Digital Library

[7]

Augustin, L. M., Gennart, B. A., Huh, Y., Luckham, D. C. and Stanculescu, A., VAL: An Annotation Language for VHDL. in International Conference on Computer-Aided Design, (1987), IEEE Computer Society, 418--421.

[8]

Bates, P. C. and Wileden, J. C. High-Level Debugging of Distributed Systems: The Behavioral Abstraction Approach. Journal of Systems and Software, 3. 255--264.

Digital Library

[9]

Beyer, D., Chlipala, A. J., Henzinger, T. A., Jhala, R. and Majumdar, R., The Blast Query Language for Software Verification. in Proceedings of the 11th International Static Analysis Symposium (2004), Springer-Verlag, 2--18.

[10]

Bjørner, D. and Jones, C. B. The Vienna Development Method: The Meta-Language. Springer-Verlag, 1978.

[11]

Blum, M. and Kannan, S. Designing Programs that Check Their Work. Journal of the ACM, 42 (1). 269--291.

Digital Library

[12]

Chalin, P. Ensuring Continued Mainstream Use of Formal Methods: An Assessment, Roadmap and Issues. Group, D. S. R. ed., Concordia University, 2005.

[13]

Cline, M. P. and Lea, D., Using Annotated C++. in C++ at Work Conference, (1990).

[14]

Cook, J., Assertions for the Tcl Language. in Fifth Tcl Workshop, (Boston, MA, 1997), 73--80.

Digital Library

[15]

Cusumano, M. A. and Selby, R. W. Microsoft Secrets: How the World's Most Powerful Software Company Creates Technology, Shapes Markets, and Manages People. Free Press, New York, NY, 1995.

Digital Library

[16]

Deutsch, L. P. An Interactive Program Verifier, University of California, Berkeley, Berkeley, CA, 1973.

[17]

Dijkstra, E. W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, 1976.

Digital Library

[18]

Dijkstra, E. W. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM, 18 (8). 453--457.

Digital Library

[19]

Dillon, L. K., Kutty, G., Moser, L. E., Melliar-Smith, P. M. and Ramakrishna, Y. S. A Graphical Interval Logic for Specifying Concurrent Systems. ACM Transactions on Software Engineering and Methodology, 3 (2). 131--165.

Digital Library

[20]

Elbaum, S. and Diep, M. Profiling Deployed Software: Assessing Strategies and Testing Opportunities. Transactions on Software Engineering, 31 (4). 312--327.

Digital Library

[21]

Ernst, M. D., Cockrell, J., Griswold, W. G. and Notkin, D. Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Transactions on Software Engineering, 27 (2). 1--25.

Digital Library

[22]

Evans, T. G. and Darley, D. L., On-Line Debugging Techniques: A Survey. in AFIPS Fall Joint Computer Conference, (1966), 37--50.

Digital Library

[23]

Findler, R. B., Latendresse, M. and Felleisen, M., Behavioral Contracts and Behavioral Subtyping. in Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Vienna, Austria, 2001), 229--236.

Digital Library

[24]

Flater, D. W., Yesha, Y. and Park, E. K. Extensions to the C Programming Language for Enhanced Fault Detection. Software-Practice and Experience, 23 (6). 617--628.

Digital Library

[25]

Floyd, R. W., Assigning Meaning to Programs. in Symposium on Applied Mathematics, (New York, 1967), American Mathematical Society, 19--32.

[26]

Gautron, P., An Assertion Mechanism Based on Exceptions. in Fourth C++ Technical Conference, (1992), USENIX Association, 245--262.

[27]

Goldstine, H. H. and Von Neumann, J. Planning and Coding Problems for an Electronic Computing Instrument. in Taub, A. H. ed. Jon von Neumann, Collected Works, Pergamon Press, London, England, 1963, 80--235.

[28]

Good, D. I., London, R. L. and Bledsoe, W. W. An Interactive Program Verification System. IEEE Transactions on Software Engineering, SE-1. 59--67.

Digital Library

[29]

Goodenough, J. B. Exception Handling: Issues and a Proposed Notation. Communications of the ACM, 18 (12). 683--696.

Digital Library

[30]

Gosling, J., Joy, B. and Steele, G. The Java(TM) Language Specification. Addison-Wesley, 1996.

Digital Library

[31]

Gries, D. The Science of Programming. Springer-Verlag, New York, 1981.

Digital Library

[32]

Hantler, S. and King, J. An Introduction to Proving the Correctness of Programs. ACM Computing Surveys, 8 (3). 331--353.

Digital Library

[33]

Haran, M., Karr, A., Orso, A., Porter, A. and Sanali, A., Applying Classification Techniques to Remotely-collected Program Execution Data. in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, (Lisbon, Portugal, 2005), ACM SIGSOFT, 146--155

Digital Library

[34]

Helmbold, D. P. and Luckham, D. C. Debugging Ada Tasking Programs. IEEE Software, 2 (2). 47--57.

Digital Library

[35]

Hoare, C. A. R. An Axiomatic Basis of Computer Programming. Communications of the ACM, 12 (10). 576--580.

Digital Library

[36]

Hoare, C. A. R. Assertions: A Personal Perspective. IEEE Annals of the History of Computing, 25 (2). 14--25.

Digital Library

[37]

Holt, R. C. and Cordy, J. R. The Touring Programming Language. Communications of the ACM, 31 (12). 1410--1423.

Digital Library

[38]

Holzmann, G. J. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23 (5). 279--294.

Digital Library

[39]

Holzmann, G. J. The SPIN Model Checker. Addison-Wesley, 2004.

[40]

Igarashi, S., London, R. L. and Luckham, D. C. Automatic Program Verification I: A Logical Basis and its Implementation. Acta Informatica, 4. 145--182.

[41]

Jones, C. B. Systematic Software Development Using VDM. Prentice-Hall International, 1990.

Digital Library

[42]

Jones, C. B. The Early Search for Tractable Ways of Reasoning about Programs. IEEE Annals of the History of Computing, 25 (2). 26--49.

Digital Library

[43]

King, J. C. A Program Verifier, Carnegie Mellon University, Pittsburgh, PA, 1969.

[44]

Leveson, N. G., Cha, S. S., Knight, J. C. and Shimeall, T. J. The Use of Self Checks and Voting in Software Error Detection: An Empirical Study. IEEE Transactions on Software Engineering, SE-16 (4). 432--443.

Digital Library

[45]

Liblit, B., Aiken, A., Zheng, A. and Jordan, M., Bug Isolation via Remote Program Sampling. in Programming Language Design and Implementation, (San Diego, CA, 2003), ACM SIGPLAN, 141--154

Digital Library

[46]

Linger, R. C., Mills, H. D. and Witt, B. I. Structured Programming: Theory and Practice. Addison-Wesley, 1979.

Digital Library

[47]

Liskov, B. and Guttag, J. Abstraction and Specification in Program Development. MIT Press, 1986.

Digital Library

[48]

Liskov, B. H. and Wing, J. M. A Behavioral Notion of Subtyping. ACM Transactions on Programming Languages and Systems, 16 (6). 1811--1841.

Digital Library

[49]

Luckham, D. C. Programming with Specifications: An Introduction to Anna, a Language for Specifying Ada Programs. Springer-Verlag, 1990.

Digital Library

[50]

Luckham, D. C., German, S. M., vonHenke, F. W., Karp, R. A., Milne, P. W., Oppen, D. C., Polak, W. and Scherlis, W. L. Stanford Pascal Verifier User Manual, Department of Computer Science, Stanford University, 1979.

Digital Library

[51]

Luckham, D. C., Helmbold, D. P., Bryan, D. L. and Haberler, M. A., Task Sequencing Language for Specifying Distributed Ada Systems (TSL-1). in PARLE---The Conference on Parallel Architectures and Languages Europe, Volume II: Parallel Languages, (1987), Springer-Verlag, 444--463.

Digital Library

[52]

Luckham, D. C., Kenney, J. J., Augustin, L. M., Vera, J., Bryan, D. and Mann, W. Specification and Analysis of System Architecture Using Rapide. IEEE Transactions on Software Engineering, 21 (4). 336--355.

Digital Library

[53]

Luckham, D. C. and vonHenke, F. W. An Overview of Anna: a Specification Language for Ada. IEEE Software, 2 (2). 9--24.

Digital Library

[54]

Mahmood, A. and McCluskey, E. J. Concurrent Error Detection Using Watchdog Processors---A Survey, Computer Systems Laboratory, Stanford University, 1985.

[55]

Maker, P. J. GNU Nana User's Guide, Version 2.4, School of Information Technology, Northern Territory University, 1998.

[56]

Manna, Z. Properties of Programs and the First-Order Predicate Calculus. Journal of the ACM 16 (2). 244--255.

Digital Library

[57]

Manna, Z. and Pnueli, A. Verification of Concurrent Programs: The Temporal Framework. in Boyer, R. S. and J. S. Moore eds. The Correctness Problem in Computer Science, Academic Press, London, 1981, 215--273.

[58]

McCarthy, J., Towards a Mathematical Science of Computation. in IFIP Congress 62, (1963), North-Holland.

[59]

Meyer, B. Applying 'Design by Contract'. IEEE Computer, 25 (10). 40--51.

Digital Library

[60]

Meyer, B. Eiffel: A Language and Environment for Software Engineering. Journal of Systems and Software, 8 (3). 199--246.

Digital Library

[61]

Meyer, B. Eiffel: The Language. Prentice Hall, 1991.

Digital Library

[62]

Meyer, B. Personal communication. Clarke, L. and Rosenblum, D. eds., 2005.

[63]

Müller, M. M., Typke, R. and Hagner, O., Two Controlled Experiments Concerning the Usefulness of Assertions as a Means for Programming. in International Conference on Software Maintenance, (Montreal, Canada, 2002), 84--92.

Digital Library

[64]

Musser, D. R., Abstract Data Type Specification in the Affirm System. in Specifications of Reliable Software, (Cambridge, MA, 1979), IEEE Computer Society, 47--57.

[65]

Naur, P. Proof of Algorithms by General Snapshots. BIT, 6. 310--316.

[66]

OMG. OCL 2.0 Specification, Version 2.0, Object Management Group, Framingham, MA, 2005.

[67]

OMG. Unified Modeling Language (UML) Version 1.4.2, Object Management Group, Framingham, MA, 2001.

[68]

Osterweil, L. J. Using Data Flow Tools in Software Engineering. in Muchnick and Jones eds. Progarm Flow Analysis: Theory and Application, Prentice-Hall, Englewood Cliff, N. J., 1981.

[69]

Parasoft. Jcontract, 2004.

[70]

Parnas, D. L. A Technique for Software Module Specification with Examples. Communications of the ACM, 15 (5). 330--336.

Digital Library

[71]

Pnueli, A., The Temporal Logic of Programs. in Eighteenth Symposium on Foundations of Computer Science, (Providence, RI, 1977), 46--57.

[72]

Popek, G. J., Horning, J. J., Lampson, B. W., Mitchell, J. G. and London, R. L., Notes on the Design of Euclid. in ACM Conference on Language Design for Reliable Software, (Raleigh, North Carolina, 1977), 11--18.

Digital Library

[73]

Quality Week, in International Quality Week, (San Francisco, CA, 1987 - 2006), Software Research Institute.

[74]

Rosenblum, D. S. A Practical Approach to Programming with Assertions. IEEE Transactions on Software Engineering, 21 (1). 19--31.

Digital Library

[75]

Rosenblum, D. S., Sankar, S. and Luckham, D. C., Concurrent Runtime Checking of Annotated Ada Programs. in Sixth Conference on Foundations of Software Technology and Theoretical Computer Science, (New Delhi, India, 1986), Springer-Verlag, 10--35.

Digital Library

[76]

Ryder, B. G. The PFORT Verifier. Software --- Practice and Experience, 4. 359--378.

[77]

Salvador, R. Personal communication with VP of Research and Development at Parasoft. Clarke, L. and Rosenblum, D. eds., 2006.

[78]

Sankar, S., Run-Time Consistency Checking of Algebraic Specifications. in The 4th Software Testing, Analysis and Verification Symposium, (1991), ACM SIGSOFT, 123--129.

Digital Library

[79]

Sankar, S. and Rosenblum, D. S. Runtime Checking and Debugging of Formally Specified Programs. ACM Computing Surveys, 23 (1). 125--127.

Digital Library

[80]

Sankar, S., Rosenblum, D. S. and Neff, R. B., An Implementation of Anna. in Ada in Use: The Ada International Conference, (1985), Cambridge University Press, 285--296.

Digital Library

[81]

Schwartz, R. L., Melliar-Smith, P. M. and Vogt, F. H., An Interval Logic for Higher-Level Temporal Reasoning. in 2nd Symposium on Principles of Distributed Computing, (1983), ACM SIGOPS, 173--186.

Digital Library

[82]

Spivey, J. M. Introducing Z: A Specification Language and its Formal Semantics. Cambridge University Press, Cambridge, MA, 1988.

Digital Library

[83]

Spivey, J. M. The Z Notation A Reference Manual. Prentice Hall International Series in Computer Science, Englewood Cliffs, NJ, 1992.

Digital Library

[84]

Spivey, J. M. The Z Notation: A Reference Manual. Prentice Hall International, Englewood Cliffs, NJ, 1989.

Digital Library

[85]

Stucki, L. G., Automatic Generation of Self-Metric Software. in IEEE Symposium on Software Reliability, (1973), IEEE Computer Society, 94--100.

[86]

Stucki, L. G. and Foshee, G. L., New Assertion Concepts in Self-metric Software Validation. in 1975 International Conference on Reliable Software, (1975), 59--71.

Digital Library

[87]

Sun Microsystems, I. Programming with Assertions, 2002.

[88]

Tardo, J. and Goguen, J. A., An Introduction to OBJ: a Language for Writing and Testing Algebraic Specifications. in Specifications of Reliable Software, (Cambridge, MA, 1979), 170--189.

[89]

Thompson, K. and Ritchie, D. M. UNIX Programmer's Manual. Murray Hill, NJ, 1979.

[90]

Turing, A., Checking a Large Routine. in Conference on High Speed Automatic Calculating Machines, (Cambridge, UK, 1949), 67--69.

[91]

Wegbreit, B. Constructive Methods in Program Verification. IEEE Transactions on Software Engineering, SE- 3. 193--209.

[92]

Wirth, N. and Hoare, C. A. R. A Contribution to the Development of Algol. Communications of the ACM, 9 (6). 413--431.

Digital Library

[93]

Wulf, W. A., London, R. L. and Shaw, M. An Introduction to the Construction and Verification of Alphard Programs. IEEE Transactions on Software Engineering, SE-2 (4). 253--265.

Digital Library

[94]

Yau, S. S. and Cheung, R. C., Design of Self-Checking Software. in International Conference on Reliable Software, (1975), ACM and IEEE Computer Society, 450--457.

Digital Library

[95]

Yin, H. and Bieman, J. M., Improving Software Testability with Assertion Insertion. in International Test Conference, (1994), 831--839.

Digital Library

[96]

Zuse, K. Der Plankalkül, Gesellschaft für Mathematik und Datenverarbeitung, 1972.

Cited By

Leeson WDwyer M(2024)Algorithm Selection for Software Verification Using Graph Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/363722533:3(1-36)Online publication date: 14-Mar-2024
https://dl.acm.org/doi/10.1145/3637225
Soares TChirica IPereira M(2024)Static and Dynamic Verification of OCaml Programs: The Gospel EcosystemLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_14(247-265)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_14
Ziani YKosmatov NLoulergue FGracia Pérez D(2024)Runtime Verification for High-Level Security Properties: Case Study on the TPM Software StackTests and Proofs10.1007/978-3-031-72044-4_5(87-106)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72044-4_5
Show More Cited By

Index Terms

A historical perspective on runtime assertion checking in software development

Recommendations

Efficient runtime assertion checking of assignable clauses with datagroups
FASE'10: Proceedings of the 13th international conference on Fundamental Approaches to Software Engineering

Runtime assertion checking is useful for debugging programs and specifications. Existing tools check invariants as well as method pre- and postconditions, but mostly ignore assignable (or modifies) clauses, which specify the heap locations a method is ...
The e-ACSL perspective on runtime assertion checking
VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution

Runtime Assertion Checking (RAC) is the discipline of verifying program assertions at runtime, i.e. when executing the code. Nowadays, RAC usually relies on Behavioral Interface Specification Languages (BISL) à la Eiffel for writing powerful code ...
Ortac: Runtime Assertion Checking for OCaml (Tool Paper)
Runtime Verification
Abstract
Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime.
In this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 3

May 2006

171 pages

ISSN:0163-5948

DOI:10.1145/1127878

Issue’s Table of Contents

Copyright © 2006 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2006

Published in SIGSOFT Volume 31, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

123
Total Citations
View Citations
1,088
Total Downloads

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

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Leeson WDwyer M(2024)Algorithm Selection for Software Verification Using Graph Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/363722533:3(1-36)Online publication date: 14-Mar-2024
https://dl.acm.org/doi/10.1145/3637225
Soares TChirica IPereira M(2024)Static and Dynamic Verification of OCaml Programs: The Gospel EcosystemLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_14(247-265)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_14
Ziani YKosmatov NLoulergue FGracia Pérez D(2024)Runtime Verification for High-Level Security Properties: Case Study on the TPM Software StackTests and Proofs10.1007/978-3-031-72044-4_5(87-106)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72044-4_5
Kosmatov NPlaunov AShankar SSignoles J(2024)Combining Analyses Within Frama-CGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_9(423-455)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_9
Benjamin TSignoles J(2024)Runtime Annotation Checking with Frama-C: The E-ACSL Plug-inGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_5(263-303)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_5
Iyer RKalbarczyk ZNakka N(2024)Hardware Error Detection Through Software‐Implemented TechniquesDependable Computing10.1002/9781119743453.ch5(141-178)Online publication date: 26-Apr-2024
https://doi.org/10.1002/9781119743453.ch5
Nilizadeh ALeavens GPăsăreanu CNoller Y(2023)JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion CheckingFormal Aspects of Computing10.1145/360753836:1(1-24)Online publication date: 5-Aug-2023
https://dl.acm.org/doi/10.1145/3607538
Ly DKosmatov NLoulergue FSignoles J(2023)Sound Runtime Assertion Checking for Memory Properties via Program TransformationFormal Aspects of Computing10.1145/360595136:1(1-46)Online publication date: 31-Jul-2023
https://dl.acm.org/doi/10.1145/3605951
Coullon HHenrio LLoulergue FRobillard S(2023)Component-based Distributed Software Reconfiguration:A Verification-oriented SurveyACM Computing Surveys10.1145/359537656:1(1-37)Online publication date: 26-Aug-2023
https://dl.acm.org/doi/10.1145/3595376
Kotti ZGousios GSpinellis D(2023)Impact of Software Engineering Research in Practice: A Patent and Author Survey AnalysisIEEE Transactions on Software Engineering10.1109/TSE.2022.320821049:4(2020-2038)Online publication date: 1-Apr-2023
https://doi.org/10.1109/TSE.2022.3208210
Show More Cited By

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.

Media

Figures

Other

Tables

View Issue’s Table of Contents