Article

Model checking software with well-defined APIs: the socket case

Authors:

P. de la Cámara,

M. M. Gallardo,

D. SanánAuthors Info & Claims

FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems

Pages 17 - 26

https://doi.org/10.1145/1081180.1081184

Published: 05 September 2005 Publication History

Abstract

The application of model checking technology to real software seems to be a promising and realistic approach to increase its quality. There are some successful examples of tools for this purpose, mainly working with self-contained programs. However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend.In this paper, we give a method for using the tool SPIN to verify distributed software systems that use the API Socket and the network protocol stack TCPIP for communications. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker. We define and use a formal semantics of the API to conduct the correct construction of models. The whole modelling process is transparent to the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we ensure that the system only reports potential (non-spurious) errors.

References

[1]

T. Ball, B. Cook, V. Levin, S.K. Rajamani: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: IFM. (2004)

[2]

T. Ball, R. Mjumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN '01 Conference on Programming Language Design and Implementation, 2001

Digital Library

[3]

T. Ball, A. Podelski, S. K. Rajamani. Boolean and Cartesian Abstractions for Model Checking C Programs, TACAS 01:Tools and Algorithms for Construction and Analysis of Systems, LNCS 2031, pages. 268--283. Springer-Verlag, 2001

Digital Library

[4]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, volume 2988 of LNCS, pages 168--176. Springer, 2004.

[5]

M. M. Gallardo, P. Merino, E. Pimentel. A Generalized Semantics of Promela for Abstract Model Checking. Formal Aspects of Computing (2004) 16: 166--193

[6]

M. M. Gallardo, J. Martinez, P. Merino, E. Pimentel. αSPIN: A Tool for Abstract Model Checking. Int. J. on Software Tools for Technology Transfer, 5 (2-3),pp. 165 -- 184, 2004.

Digital Library

[7]

P. Godefroid. Model Checking for Programming Languages using Verisoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, 1997

Digital Library

[8]

G. J. Holzmann. The Model Checker SPIN. IEEE Trans. on SE, 23(5), (1997).

Digital Library

[9]

G.J. Holzmann. SPIN Model Checker, The: Primer and Reference Manual. Addison Wesley, 2004.

Digital Library

[10]

G. J. Holzmann and M. Smith. Software model checking. Extracting verification models from source code. In Invited Paper. Proc. PSTV/FORTE99 Pulb. Kluwer, 1999

Digital Library

[11]

K. Havelund, Thomas Pressburger. Model Checking Java Programs Using Java PathFinder. In International Journal on Software tools for Technology Transfer (STTT), 1999.

[12]

Java Compiler Compiler: The Java Parser Generator. Online documentation for version 0.7.1. Sun Microsystems. Available at http://www.sun.com/suntest/JavaCC

[13]

J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting Finitestate Models from Java Source Code. In Proc. of the 22nd Int. Conf. on Software Engineering, 2000, ACM Press.

Digital Library

[14]

M. Musuvathi, D. W. Park, A. Chou, D. R. Engler, D. L. Dill. CMC: A Pragmatic Approach to Model Checking Real Code. In Proc. of the Fifth Symposium on Operating Systems Design and Implementation, 2002.

Digital Library

[15]

S. D. Stoller. Model-Checking Multi-Threaded Distributed Java Programs. In Proc. 11th International Conference on Automated Deduction, LNAI-607 pages 748--752, 1992.

[16]

W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proc. of the 15th Int. Conf. on Automated Software Engineering, pages 3--12. IEEE Comp. Society, 2000.

Digital Library

Cited By

Lång JPrasetya IDumas MPfahl DApel SRusso A(2019)Model checking a C++ software framework: a case studyProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3340453(1026-1036)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3340453
Sebih NHagiya MWeitl FYamamoto MArtho CTanabe Y(2015)Software Model Checking of UDP-based Distributed ApplicationsInternational Journal of Networking and Computing10.15803/ijnc.5.2_3735:2(373-402)Online publication date: 2015
https://doi.org/10.15803/ijnc.5.2_373
Yamada CMiller D(2015)Using SPIN to check Simulink Stateflow models2015 IEEE/ACIS 14th International Conference on Computer and Information Science (ICIS)10.1109/ICIS.2015.7166587(161-166)Online publication date: Jun-2015
https://doi.org/10.1109/ICIS.2015.7166587
Show More Cited By

Index Terms

Model checking software with well-defined APIs: the socket case

Recommendations

Model Checking Process with Goal Oriented Requirements Analysis
APSEC '08: Proceedings of the 2008 15th Asia-Pacific Software Engineering Conference

Model checking is a powerful technique for verifying the correctness of a system’s specification. But even when the specification has been verified to be correct, there is still the question of whether the specification covers all the expected ...
Model checking XML manipulating software
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems

September 2005

152 pages

ISBN:1595931481

DOI:10.1145/1081180

General Chairs:
Tiziana Margaria
Universitat Gottingen, Germany
,
Mieke Massink
CNR-ISTI, Italy

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

FMICS05

Sponsor:

FMICS05: Tenth International Workshop on Formal Methods in Industrial Criticial Systems 2005

September 5 - 6, 2005

Lisbon, Portugal

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
394
Total Downloads

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

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lång JPrasetya IDumas MPfahl DApel SRusso A(2019)Model checking a C++ software framework: a case studyProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3340453(1026-1036)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3340453
Sebih NHagiya MWeitl FYamamoto MArtho CTanabe Y(2015)Software Model Checking of UDP-based Distributed ApplicationsInternational Journal of Networking and Computing10.15803/ijnc.5.2_3735:2(373-402)Online publication date: 2015
https://doi.org/10.15803/ijnc.5.2_373
Yamada CMiller D(2015)Using SPIN to check Simulink Stateflow models2015 IEEE/ACIS 14th International Conference on Computer and Information Science (ICIS)10.1109/ICIS.2015.7166587(161-166)Online publication date: Jun-2015
https://doi.org/10.1109/ICIS.2015.7166587
de la Cámara PCastro JGallardo MMerino P(2010)Verification support for ARINC-653-based avionics softwareSoftware Testing, Verification and Reliability10.1002/stvr.42221:4(267-298)Online publication date: 18-Jan-2010
https://doi.org/10.1002/stvr.422
Cámara PMar Gallardo MMerino PSanán D(2009)Checking the reliability of socket based communication softwareInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220885.322100911:5(359-374)Online publication date: 1-Nov-2009
https://dl.acm.org/doi/10.5555/3220885.3221009
Rolando PSisto R(2009)An experience in embedded control software verification2009 IEEE Conference on Emerging Technologies & Factory Automation10.1109/ETFA.2009.5347235(1-4)Online publication date: Sep-2009
https://doi.org/10.1109/ETFA.2009.5347235
Gallardo MMerino PSanán D(2009)Model Checking Dynamic Memory Allocation in Operating SystemsJournal of Automated Reasoning10.1007/s10817-009-9124-y42:2-4(229-264)Online publication date: 1-Apr-2009
https://dl.acm.org/doi/10.1007/s10817-009-9124-y
del Mar Gallardo MMerino PSánan D(2008)Model Checking C Programs with Dynamic Memory AllocationProceedings of the 2008 32nd Annual IEEE International Computer Software and Applications Conference10.1109/COMPSAC.2008.143(219-226)Online publication date: 28-Jul-2008
https://dl.acm.org/doi/10.1109/COMPSAC.2008.143
del Mar Gallardo MJoubert CMerino PSanán D(2007)C.OPEN and ANNOTATORProceedings of the 14th international SPIN conference on Model checking software10.5555/1770532.1770557(268-273)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.5555/1770532.1770557
de la Cámara Pdel Mar Gallardo MMerino P(2007)Model extraction for ARINC 653 based avionics softwareProceedings of the 14th international SPIN conference on Model checking software10.5555/1770532.1770554(243-262)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.5555/1770532.1770554
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 Table of Contents