Loading...
Please wait, while we are loading the content...
Similar Documents
A Methodology to Detect ” Hard-to-Find ” bugs in Large Multithreaded Java Programs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Sreeranga P. Rajan Sidle, Thomas Fujitsu |
| Copyright Year | 2004 |
| Abstract | Multithreaded programming has become increasingly essent ial for developing highly efficient software. Concurrency in multi threaded programs introduces additional complexity in software ver ification and testing, and thereby significantly increasing the cost o f Quality Assurance (QA). In this report we describe the verification o f enterprise client-server Business Process Management (BPM)/wo rkflow software. We developed a practical verification methodolog y using a formal analysis tool called Java PathFinder (JPF) from NAS A with special emphasis on finding deadlocks and race conditio s. The results revealed race conditions that lead to data corru ption errors whose detection would have been prohibitively expensi v with conventional testing and QA methods. To the best of our knowl edge, this is the first time a methodology involving formal an alysis has been successfully applied to such a large client-server software project. 1. BACKGROUND AND HISTORY Sree Rajan and Tom Sidle of Advanced CAD Department, Fujitsu Laboratories of America (FLA), initiated the contact with K eith Swenson, Chief Scientist and Architect of Interstage Busin ess Process Management (I-BPM) and Director of Fujitsu Software Corpor ation in 2003. In this meeting we concluded that there was scop e for applying formal verification techniques to detect deadl ocks and race conditions in Fujitsu’s workflow client-server Java so ftware. We established research links with Willem Visser of NASA and obtained the model checking tool called Java Path Finder (JP F) for trial purposes. We then had several meetings with the softwa re development team and did preliminary trials on applying JPF to the workflow software. As it is well known that applying formal mo del checking tools to large software or hardware designs fail, w e came up with a strategy to apply model checking only to portions of the large workflow software with promising results. In July 2004 , we attended the Computer-Aided Verification (CAV) conference and met with Willem Visser. With his acceptance to collaborate i n the software verification of a real large software product, NASA agreed to support our software verification activity in providing J PF and also funding for a student intern if requested. After a month -long search for a competent doctoral student researcher, Graham Hughes ** This is the first time a successful attempt has been made in a pplying formal analysis for finding bugs in very large client-server ind ustrial strength software. Interstage Business Process Management (I-BPM) software developed and marketed by Fujitsu Software Corporation is a co mplex and mature product, with more than 1500 classes spanning more th an 500,000 lines of Java code. The challenge in finding bugs in such a larg e software program is as hard as finding a small needle in big haystack. Ou r methodology has helped increase the quality of the product in the field . All the bugs reported in this memo have or had been fixed in the field. from UCSB accepted to visit us starting August 23, 2004 for a f ew months to work on verifying I-BPM software using JPF. Initia lly, the most difficult part was how to select portions of the I-BPM code on which we need to perform model checking. I-BPM is a complex and mature product, with more than 1500 classes spanning mor e than 500,000 lines of Java code. We were challenged to discov er deadlocks and race conditions in the cache and other portion s of IBPM that they could not find using conventional tools. We met t his challenge successfully in 5 weeks by the end of September 200 4. Our methodology has helped increase the quality of the produ ct in the field, thereby demonstrating the effectiveness of forma l an lysis in detecting complex concurrency bugs. All the bugs repo rt d in this memo have or had been fixed in the field. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://kswenson.purplehillsbooks.com/2004/TM-233-fujitsu.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
