Automatic verification of time behavior of programs
Pages 468 - 471
Abstract
Automatic verification of software could save companies from huge losses due to errors in their programs. Existing techniques to prevent and detect errors are mainly based on imprecise heuristics which can report false positives. Formal verification techniques are an alternative to the heuristic approaches. They are more precise and can report errors with higher rigor. However, they cannot be directly applied because current programming languages have no defined semantics that specifies how the source code is interpreted in the execution of programs. Moreover, no existing work tries to develop a semantics for the time domain. The target of this thesis is to provide a verification framework based on a defined time semantics that can help developers to automatically detect time related errors in the behavior of programs. We define a time semantics that allows us to ascribe a meaning to source code statements that alter and use time. Based on the time semantics, we develop an approach to (i) automatically assert time properties and (ii) reverse engineer timed automata, a formal model of the time behavior that is amenable for verification. We plan to evaluate our approaches with quantitative and qualitative studies. The quantitative studies will measure the performance of our approaches in open source projects and the qualitative studies will collect the developers' feedback about the applicability and usefulness of our proposed techniques.
References
[1]
Rajeev Alur and David L Dill. 1994. A theory of timed automata. Theoretical computer science 126, 2 (1994), 183--235.
[2]
C Artho. 2006. JLint - Find Bugs in Java Programs. (2006). http://jlint.sourceforge.net/.
[3]
Denis Bogdanas and Grigore Roşu. 2015. K-Java: A Complete Semantics of Java. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 445--456.
[4]
Marat Boshernitsan, Roongko Doong, and Alberto Savoia. 2006. From Daikon to Agitator: lessons and challenges in building a commercial tool for developer testing. In Proceedings of the 2006 international symposium on Software testing and analysis (ISSTA). ACM, 169--180.
[5]
Robert N Charette. 2005. Why software fails. IEEE spectrum 42, 9 (2005), 1--36.
[6]
John W Creswell. 2013. Research design: Qualitative, quantitative, and mixed methods approaches. Sage publications.
[7]
Azadeh Farzan, Feng Chen, José Meseguer, and Grigore Roşu. 2004. Formal analysis of Java programs in JavaFAN. In International Conference on Computer Aided Verification. Springer, 501--505.
[8]
Chryssis Georgiou, Peter M Musial, and Christos Ploutarchou. 2013. Tempo-toolkit: Tempo to Java Translation Module. In International Symposium on Network Computing and Applications (NCA). IEEE, 235--242.
[9]
Niusha Hakimipour, Paul Strooper, and Andy Wellings. 2010. TART: Timed-automata to real-time Java tool. In International Conference on Software Engineering and Formal Methods (SEFM). IEEE, 299--309.
[10]
John Hatcliff and Matthew Dwyer. 2001. Using the Bandera tool set to model-check properties of concurrent Java software. In International Conference on Concurrency Theory (CONCUR). Springer, 39--58.
[11]
Chris Hathhorn, Chucky Ellison, and Grigore Roşu. 2015. Defining the Undefinedness of C. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15). ACM, 336--345.
[12]
Klaus Havelund and Thomas Pressburger. 2000. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer (STTT) 2, 4 (2000), 366--381.
[13]
Nikolas Havrikov, Alessio Gambi, Andreas Zeller, Andrea Arcuri, and Juan Pablo Galeotti. 2017. Generating unit tests with structured system interactions. In Proceedings of the 12th International Workshop on Automation of Software Testing (AST). IEEE Press, 30--33.
[14]
Thomas A Henzinger, George C Necula, Ranjit Jhala, Gregoire Sutre, Rupak Majumdar, and Westley Weimer. 2002. Temporal-safety proofs for systems code. In International Conference on Computer Aided Verification (CAV). Springer, 526--538.
[15]
David Hovemeyer and William Pugh. 2004. Finding bugs is easy. ACM Sigplan Notices 39, 12 (2004), 92--106.
[16]
Michael Jackson. 1995. The world and the machine. In Proceedings of the 17th international conference on Software engineering. ACM, 283--292.
[17]
Swaminathan Jayaraman, Dinoop Hari, and Bharat Jayaraman. 2015. Consistency of Java run-time behavior with design-time specifications. In International Conference on Contemporary Computing (IC3). IEEE, 548--554.
[18]
Kim G Larsen, Paul Pettersson, and Wang Yi. 1997. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer (STTT) 1, 1--2 (1997), 134--152.
[19]
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2014. The CompCert memory model. In Program Logics for Certified Compilers, Andrew W. Appel (Ed.). Cambridge University Press.
[20]
Giovanni Liva, Muhammad Taimoor Khan, and Martin Pinzger. 2017. Extracting timed automata from Java methods. In Proceedings of the 17th International Working Conference on Source Code Analysis and Manipulation (SCAM). IEEE, 91--100.
[21]
José Meseguer and Grigore Roşu. 2011. The rewriting logic semantics project: A progress report. In International Symposium on Fundamentals of Computation Theory. Springer, 1--37.
[22]
Carlos Pacheco and Michael D Ernst. 2005. Eclat: Automatic generation and classification of test inputs. In Proceedings of the 19th European conference on Object-Oriented Programming (ECOOP). Springer-Verlag, 504--527.
[23]
Carlos Pacheco and Michael D Ernst. 2007. Randoop: feedback-directed random testing for Java. In Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion (OOPSLA). ACM, 815--816.
[24]
Carlos Pacheco, Shuvendu K Lahiri, and Thomas Ball. 2008. Finding errors in. net with feedback-directed random testing. In Proceedings of the 2008 international symposium on Software testing and analysis (ISSTA). ACM, 87--96.
[25]
Carlos Pacheco, Shuvendu K Lahiri, Michael D Ernst, and Thomas Ball. 2007. Feedback-directed random test generation. In Proceedings of the 29th international conference on Software Engineering (ICSE). IEEE Computer Society, 75--84.
[26]
Philip E Ross. 2005. The exterminators {software bugs}. IEEE spectrum 42, 9 (2005), 36--41.
[27]
Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397--434.
[28]
Robert F Stärk, Joachim Schmid, and Egon Börger. 2012. Java and the Java virtual machine: definition, verification, validation. Springer Science & Business Media.
[29]
R Hevner Von Alan, Salvatore T March, Jinsoo Park, and Sudha Ram. 2004. Design science in information systems research. MIS quarterly 28, 1 (2004), 75--105.
[30]
Yixiao Yang, Yu Jiang, Ming Gu, and Jiaguang Sun. 2016. Verifying simulink stateflow model: timed automata approach. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM, 852--857.
Recommendations
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Refinement-Based Verification of Interactive Real-Time Systems
Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with ...
Formal Verification of Ada Programs
The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification ...
Comments
Information & Contributors
Information
Published In
May 2018
231 pages
ISBN:9781450356633
DOI:10.1145/3183440
- Conference Chair:
- Michel Chaudron,
- General Chair:
- Ivica Crnkovic,
- Program Chairs:
- Marsha Chechik,
- Mark Harman
Copyright © 2018 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 the author(s) 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
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS: Computer Society
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 27 May 2018
Check for updates
Qualifiers
- Short-paper
Funding Sources
- FFG
Conference
ICSE '18
Sponsor:
- SIGSOFT
- IEEE-CS
ICSE '18: 40th International Conference on Software Engineering
May 27 - June 3, 2018
Gothenburg, Sweden
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 122Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)0
Reflects downloads up to 23 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in