Shyamala Lakshminarasimhan September 26, 2008 [email protected] Project proposal – CS395T Model Checking Using Java PathFinder – A Survey Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Extremely large state-spaces can often be traversed in minutes. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. Java PathFinder is a system to verify executable Java bytecode programs. In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Unlike traditional debuggers, JPF reports the entire execution path that leads to a defect. JPF is especially well-suited to finding hard-to-test concurrency defects in multi-threaded programs. It compresses and stores states in a table to prevent redundant searches and relies on various abstraction techniques to curb the state space explosion problem. Problem Statement: • What are the key features of JPF? • How does JPF work along with Java PathExplorer, a runtime verification tool? • How is JPF used as a translator for the SPIN model checker to translate from Java to PROMELA? • How is JPF used to verify finite state concurrent systems? In particular, how was it applied to detect concurrency errors in NASA's remote agent space craft controller?Project Description and Expected Results: This project will particularly focus on an analysis of model checking using Java PathFinder. It will illustrate the benefits of using Java PathFinder in multi-threaded program verification and study the architecture of JPF and how it integrates model checking, program analysis and testing. The key features of JPF would be analysed and documented and a survey of how Java PathFinder and Java PathExplorer, a runtime verification tool, work together will be undertaken. The usage of JPF as a transator for the SPIN model checker will also be studied. Finally, a case study of the application of JPF to detect concurrency errors in NASA's remote agent space craft controller will be performed. List of reference materials and tools: (The list will constantly evolve to include works that are being studied) - http://javapathfinder.sourceforge.net/ - Official Java PathFinder website - Formal Analysis of the Remote Agent Before and After Flight -http://spinroot.com/spin/Doc/rax.pdf - Tools: Java PathFinder, SPIN, Java PathExplorer Project Schedule: • The draft of the project description was submitted on 23 September 2008. The final version will be submitted on 27 September, 2008. • The research process, which includes reading documentation, exploring Java Path Finder, Java PathExplorer and SPIN, collecting background information, initial planning and designing will be completed by October 15, 2008. • Study of the application of JPF with Java PathExplorer and SPIN will be done by October 23, 2008 • The case study of the NASA's remote agent space controller concurrency error detection using JPF will be performed by November 15, 2008. • An interim report on the progress of the project will be submitted for review on the 24th of November. • A rough draft of the paper will be submitted for review on the 28th of November. • The final paper that clearly describes the study and analsyis of Java PathFinder and its features and applications will be submitted by December 2,
View Full Document
Unlocking...