Abstracts

AGEDIS Automated Model-based Test Generation and Execution for Software (Abstract) Alan Hartman, IBM HRL The AGEDIS project is a joint effort by a consortium of academic and industrial partners to improve the efficiency and effectiveness of software testing procedures. The cost of testing is estimated to be between 40% and 70% of the costs of developing a new software product. The AGEDIS project is targeting this aspect of the software development process by taking advantage of the current trend to model based software development. AGEDIS is developing a methodology and tool set for the automated generation and execution of test suites based on a specification model of the software. The methodology requires early involvement of testers in the development process, and advances the cause of design for testability through this interaction. The developers, designers, and testers cooperate in constructing a test-adequate model using UML class, object, and state diagrams. The AGEDIS tools then compile the model, to produce a simulator of the application under test. This simulator is then used by the test generator, in conjunction with a set of coverage goals and test directives to create an abstract test suite for the model. This abstract test test suite is then fed into the test execution framework along with a set of test execution directives to produce an executable test suite. This suite is distributed, synchronized, and executed to produce a trace with verdicts on the conformance of the application to the specification model. The interfaces between the components are open and available for outside groups to provide additional tools for the system. In the talk I will describe the tools and their architecture in more detail, and discuss the preliminary experiments we have carried out. Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs (Abstract) Assaf Schuster, Technion Data race detection is extremely essential for debugging multithreaded programs and assuring their correctness. Nevertheless, there is no single universal technique capable of handling the task efficiently, since data race detection is computationally hard in the general case. Thus, to approximate the possible races in a program, all currently available tools take different "short-cuts", such as using strong assumptions on the program structure, applying various heuristics, etc. When applied to some general case program, however, they usually result in excessive false positives (false alarms) or in a large amount of false negatives (undetected races). We�present a novel testing tool, called MultiRace, which combines improved versions of Djit and Lockset---two very powerful on-the-fly algorithms for dynamic detection of apparent data races. Both extended algorithms detect races in multithreaded programs that use two-way as well as global synchronization primitives---barriers and locks. MultiRace�takes advantage of the source code instrumentation idea to monitor all accesses to each of the shared locations. It requires the�C++ code of the program, but otherwise is completely transparent to the user. The main drawback of all currently available implementations of instrumentation is that they are restricted, for performance reasons, to detection units of fixed size. Thus, they all suffer from the same problem---choosing a small unit might result in missing some of the data races, while choosing a large one might lead to false detection. In contrast, by employing new technologies�of views MultiRace adjusts its detection to the native granularity of objects and variables in the program under examination. � We�describe the algorithms employed in MultiRace, as well as its implementation details. We�also propose some alternatives to and optimizations of MultiRace.�We show that the overheads imposed by�MultiRace are often much smaller (orders of magnitude) than those obtained by other existing dynamic techniques. Building Secure Code (Abstract) Oded Sacher, Microsoft Hackers cost businesses countless dollars and cause developers endless worry every year as they attack networked applications, steal credit card numbers, deface web sites, hide back doors and worms, and slow network traffic to a crawl. As soon as a new product gets into the hackers hands, they begin an intensive effort to find and exploit security holes. If the product developers don't make an at least equally intensive effort to structure security into their application, the hackers will almost surely succeed. While most of the software developers know how to design build and test product feature, they often fail in designing building and testing security. In this short presentation, we will cover: Motivation - The need for secure system will be explained. Security principals to live by. Security design by threat modeling - Identify and analyze your product assets, vulnerabilities and threats. Classify the threats by the STRIDE model: Spoofing identity Tampering with data Repudiation Information disclosure Denial of service Elevation of privileges After the threats are identified, go over some common mitigation techniques. Conducting a security push. Case Study in Abstract Testing: Checking Validity of String Operations (Abstract) Mooly Sagiv, TAU The term "abstract testing" was used by Patrick Cousot to reflect the process of statically executing a program in order to check its behavior on all possible inputs. This amounts to estimating a superset of the set of program states which may occur at runtime. Every statement (and program condition) is conservatively interpreted. This process is similar to testing but instead of executing the program on a real input, we execute it on a symbolic representation of a set of inputs. One of the nice features of abstract testing is that it can guarantee that when no errors are found, they are indeed absent (No false negatives!). However, abstract testing may yield false alarms (also called false positive) when the set of represented states also includes unfeasible behaviors. I will describe our initial experience with using abstract testing to test string operations in C programs. Specifically we very the absence of out-of-bound accesses, references beyond the null-termination byte, and invalid library calls. I will show the bugs we found and the properties we verified. Testing Multi-threaded Java Programs (Abstract) Shmuel Ur, IBM HRL It started four years ago when some colleagues spent half a man year on debugging a single "simple" bug. The main problem was that this bug appeared very rarely and was therefore very hard to locate. This frustration led to a project called ConTest whose aim is to make intermitent bugs more likely to appear and to be able to repeat execution that exhibit these bugs. The talk starts by presenting the difficulties of testing Multi-threaded programs and showing typical timing related bugs. The concepts of ConTest - an application that makes the discovery of such bugs easier by changing the relative timing of the threads - is presented. Next we demonstrate how contest is used. We conclude by showing the variety of features that where added to ConTest due to requests from the field. Information on ConTest can be seen in http://www.haifa.il.ibm.com/projects/verification/contest/index.html Directions in Formal Verification of Software (Abstract) Ishai Rabinovitz, IBM HRL Formal verification is an established methodology that can be used to check a specification over all possible execution paths of hardware or software systems. It is used to complement simulation in the hardware industry. Unfortunately, the use of formal verification on software is much harder than on hardware. Recently there has been progress in developing formal verification tools for software. In this lecture we present a brief introduction to formal verification, explain why formal verification for software is so hard, and present some basic techniques to cope with the difficulties. These techniques include boolean program abstraction and partial order reduction. Some of these techniques have been implemented in Microsoft's SLAM, Bell Labs' SPIN, Lucent's VeriSoft and Kansas University's Bandera. Model-Checking and Abstraction to the Aid of Parameterized Systems (Abstract) Amir Pnueli, Weizmann Institute of Science Keynote Parameterized systems are systems that involve numerous instantiations of the same finite-state module. Examples of parameterized systems include tele-communication protocols, bus protocols, cache coherence protocols, and many other protocols that underly current state-of-the-art systems. Our interest in Parameterized Systems stems from the fact that these are infinite-state systems which still admit (in restricted cases) algorithmic analysis. As such, they are excellent testing grounds for exploring the fine border between algorithmic and deductive verification methods. Formal verification of parameterized systems is known to be undecidable and thus cannot be automated. Recent research has shown that in many cases it is possible to use ABSTRACTION METHODS to generate a finite-state systems from a parameterized systems. The finite-state system can then be model-checked. If successful, it is possible to conclude that the original parameterized system satisfies its requirements. Otherwise, it is often the case that the counter-example produced by the model checker can indicate an error in the original parameterized system. This combined technique allows for automatic verification of parameterized systems. The talk will describe some recent approaches that combine abstraction and model-checking to verify safety as well we liveness properties of parameterized systems. We start with the method of INVISIBLE INVARIANTS that combines a small-model theorem with an heuristics to generate proofs of correctness of parameterized systems. We also describe the method of NETWORK INVARIANTS which allows to explicitly describe a finite-system that, in a precise sense, has the same external behavior as an infinite-state one, and can be used for model-checking properties. Using SW BlackBoxes to integrate root cause analysis into the QA process (Abstract) Shlomo Wygodny, Identify A common problem for QA engineers is that problems detected during testing are not always easily reproducible, or have very complicated scenario which makes their reproduction problematic. In many cases, such problems cannot be fixed because the developers cannot understand the root cause of the problem in with regular debugging methods. Using the Black Box technology, a test engineer can record the application execution, and this recording can be part of the bug report - allowing the developers to analyze the problem without reproducing it. Similarly, in load scenarios, spikes or a "knee" in the performance graph can be drilled-down to understand what happened inside the application at the time of the problem. Detecting and solving common performance problems of J2EE (Abstract) Eyal Oz, Mercury It is a well known fact that J2EE applications today consist of many different components which may reside on different machines, ending up in a pretty complex architecture. When end-users of an application experience bad performance or even wrong functionality, it is very difficult to track and detect the root cause. Oftentimes, these performance issues appear only when numerous end-users access the system all at once or at a specific constellation. Using specific tools, such as Mercury's LoadRunner can help quickly pinpoint and fix the problems. These tools offer set of views and analysis modules, starting from a high level view of each layer in the architecture, going through a layer of the specific components (such as EJBs) and drilling all the way down to the methods and SQL calls within specific components. Cross-fertilization between hardware verification and software testing (Abstract) Avi Ziv, IBM HRL To many, hardware design verification and software testing may seem like separate disciplines. Yet, significant similarities between software development and hardware design exist, and the successful adoption of techniques originally developed for one field for use in the other, suggests that these disciplines are related. One prominent crossover example is code coverage, which was first developed for software testing and is now commonly used in hardware verification. Another example is the FSM based test generator, developed for the verification of hardware modules and now successfully employed for software testing. Moreover, some techniques, such as reliability estimation, were developed for hardware, changed and adopted for software, and now start to show their usefulness with hardware again. This paper analyzes the similarities and differences between hardware verification and software testing and provides a short survey of methodologies and techniques that were developed for one field and later adapted for the other. With our knowledge and experience in both fields we try to identify other technologies from hardware verification with the potential to impact software testing.