Chester HosterDr. J.C. Browne and Dr. W. HuntCS395T Verification & Validation22 September 2008An Analysis of Model Checking and Runtime Monitoring Solutions for Library Abstraction1. Problem StatementModel checking and runtime monitoring provide valuable contributions to the verification of software systems. A key difficulty with model checking is the issue of state space explosion. System models commonly use abstractions for libraries to reduce state space. These abstractions are also useful when a model for a preexisting library is otherwise unavailable. Model checking tools may fail to discover program faults if the abstraction chosen for a library is incorrect. This is true regardless of whether the incorrect library abstraction is due to a fault in the library or an error in the choice of abstraction. These vulnerabilities at the model checking stage may be alleviated by the proper configuration of a runtime monitoring tool to reinforce the validity of the library abstraction. Which combination of model checking and runtime monitoring tools provides the best solution to library abstraction verification?2. ImplementationThe first phase of the project entails a review of appropriate background literature to identify candidate tools for model checking and runtime monitoring. The search is restricted to tools designed for Java, with preference given to those that also provide support for concurrent systems and reasonableextensibility. This phase is completed by choosing two to three tools of each type for further evaluation.The second phase of the project is the development of a small test application and an appropriate model for evaluation with the verification tools. The test application includes standardlibrary use and a library developed specifically for fault injection. The model may include minor variations depending on the requirements of the model checking tools. It is designed primarily to exercise the relationship between model checking and library abstraction.The third phase of the project is the implementation of viable tool combinations on the test application. Each model checking tool will be combined with each runtime monitoring tool to create a tool pairing. Each tool pairing is evaluated on its ability to identify faults within the test application, test library, and standard libraries. The primary focus is on faults that slip past the model checking tool and are then caught by runtime monitoring. The analysis also includes identification of areas of overlap between the tools, areas not covered by the tools, and any opportunities for automating the implementation of the runtime monitoring tool based on the prior configuration of the model checking tool. The fourth and final phase of the project is the documentation of results and the class presentation.3. Reference Materials Two to three model checking tools and the associated documentation. The preliminary candidates are SPIN and Java PathFinder. Two to three model checking tools and the associated documentation. The preliminary candidates are JPAX, MOP, and JASS. N. Delgado, A. Q. Gates, S. Roach, "A Taxonomy and Catalog of Runtime Software-Fault Monitoring Tools," IEEE Transactions on Software Engineering, vol. 30, no. 12, pp. 859-782, Dec. 2004. A. L. Williams, "Static Detection of Deadlocks for Java Libraries," Masters Thesis, MIT Department of Electrical Engineering and Computer Science, Cambridge, MA, May 2005. J. M. Hunt, J. D. McGregor, "A Model for Software Libraries," Clemson University, Sep 22 2008, <http://lcsd05.cs.tamu.edu/papers/hunt_et_al.pdf>. S. Sankar, M. Mandal, "Concurrent Runtime Monitoring of Formally Specified Programs," Computer, vol. 26, no. 3, pp. 32-41, Mar 1993. S. Chodrow, F. Jahanian, M. Donner, "RunTime Monitoring of Real-Time Systems," Real-Time Systems Symposium, 1991. Proceedings., Twelfth, pp. 74-83, Dec. 1991.4. Expected ResultsThe expected results of the project include the identification of several functional tool pairings that satisfy the requirement of supplementing library abstraction with runtime monitoring. Another result is an analysis of the relative strengths and weaknesses of each tool pairing. Tool pairings are alsoreviewed for possible extensions to increase tool coverage and automation of the runtime monitoring implementation. The creation of an end-to-end tool for supplementing library abstraction is outside of the scope of this project, however this work should serve as the basis for the creation of such a tool through the extension of the underlying tools.The target audience of this research project is the Verification and Validation course at the University of Texas. Intermediate project results are communicated via a status report. The status report includes a detailed specification of progress in each area of the project. This also includes a summary of any problems and their associated resolution or closure status. The final results of the project are delivered in the form of a conference paper. A class presentation is also used to communicate the results of the research project. The presentation includes an evaluation of the successful tool pairings, research results, and a discussion on the combination of model checking and runtime monitoring.5. Project ScheduleProject Task Expected Completion DateProposal 09/23/2008Literature Review 09/30/2008Tool Selection 10/03/2008Test Library Development 10/10/2008Test Model Development 10/17/2008Test Application Development 10/17/2008Tool Pairing Implementation 10/31/2008Project Status Report 11/05/2008Tool Pairing Analysis 11/14/2008Project Report/Paper 11/26/2008Project Presentation
View Full Document
Unlocking...