Abstracts

Thread Checker: Saving Valuable Time Otherwise Spent Searching for Hard-to-find Threading Errors (Abstract) Koby Gottlieb, Intel In this presentation, I will try to show that because of the direction of future CPUs, threading for performance will become a way of life. When threading an application, there are new sets of challenges in code quality assurance. Applications that can run correctly in the testing and validation lab might fail on exactly the same scenario after deployment. As a result of this new set of bugs, we should use new tools that might detect those bugs. I will present the Thread Checker tool that can help with cleaning those hard-to-find threading errors. The tool can find potential threading bugs even if the execution order to the code didn't expose them. I will give a short demo of the tool and try to reveal some of the secrets behind the tool's GUI. After addressing the correctness issues, we still need to get the expected performance from threading. I will give a brief description of the Thread Profiler tool that comes with the Thread Checker. This tool can help you detect the reasons for not getting the expected speedup from the threaded application. Tool-supported Methodology for Handling Multi-threaded Applications (Abstract) Eitan Farchi, IBM Haifa Labs Concurrent and distributed programs are nondeterministic. As a result, it is hard to get them right. Formal methodologies for the development of such programs have existed since the 1970s, but tool scalability problems and a lack of requisite mathematical skills among program developers have prevented their widespread use. ConTest/IRT is a test-first methodology and supporting tool set for the development of concurrent programs. In the design stage, interleavings are reviewed using the interleaving review technique, and functional coverage supports the test selection process. At the unit test level, the reviewed interleavings are reused to implement the unit test suite and obtain the required functional coverage. With ConTest, the required interleavings are much more likely to be covered, and code-based synchronization coverage is used as an exit criterion. Pilots show that the methodology is extremely effective in implementing bug-free concurrent programs. Scaling Model Checking of Dataraces Using Dynamic Information (Abstract) Ohad Shacham, IBM Haifa Labs and Tel-Aviv University Dataraces in multithreaded programs often indicate severe bugs and can cause unexpected behaviors when different thread interleavings are executed. Because dataraces are a cause for concern, many works have dealt with the problem of detecting them. Works based on dynamic techniques either report errors only for dataraces that occur in the current interleaving, which limits their usefulness, or produce many spurious dataraces. Works based on model checking search exhaustively for dataraces and thus can reveal even those that occur in rarely executed paths. However, the applicability of model checking is limited because the large number of thread interleavings in realistic multithreaded programs causes state space explosion. In this work, we combine the two techniques in a hybrid scheme, which overcomes these difficulties and enjoys the advantages of both worlds. Our experimental results show that our hybrid technique succeeds in providing a thread interleaving on realistic programs, which proves the existence of a datarace. The programs that we have experimented with cannot be checked using an ordinary industrial strength model checker or bounded model checking. Aspects and Verification: Challenges and Opportunities (Abstract) Shmuel Katz, Technion Aspects provide a modular way to describe system concerns, including security, monitoring, fault-tolerance, or evolving requirements that cross-cut normal modularity units, such as the class inheritance hierarchy in an object-oriented system. Aspects are especially useful for logging, debugging, and testing, and can also be used to help in formal verification by providing specifications. The separate description of aspects and their subsequent integration (called weaving) into systems, provide new kinds of compositionality and reuse for complex system development. But how can we show that an aspect really adds the functionality it is supposed to, and moreover does not invalidate desirable properties of the system to which it is woven? How do multiple aspects interact, and can we discover possible interference among them? In this presentation, we survey complementary approaches to the verification of systems that include aspects. One approach separates the determination of whether the aspect causes harm to the underlying system from the question of whether it adds the desired properties. We also consider when an analysis of just the aspect code is possible, and when the entire combination of the system with the aspect must be treated. Categories of aspects are defined for which static code analysis can guarantee that certain types of program properties are maintained. Multi-threaded testing with AOP is easy, and it finds bugs! (Abstract) Shady Copty, IBM Haifa Labs Aspect oriented programming (AOP) is a relatively new paradigm that has proven itself in a number of fields. We investigate the suitability of AOP for testing tools by trying to implement the ConTest testing tool using AspectJ, a tool that implements AOP for the Java programming language. Our conclusion from this exercise is that AOP is very suitable for the implementation of a number of classes of test tools. These include multi-threaded noise makers such as ConTest, in addition to coverage analyzers, data-race detectors, network traffic simulators, runtime bug pattern detectors, and others. The main advantage is that the instrumentation part of the tool creating method, which usually contains little scientific contribution but consumes most of the work, becomes much easier to perform and requires less expertise. Testing in Communication Satellite Amos 2 (Abstract) Arie Hopfeld, IAI This presentation will briefly describe the products of the Israel Aircraft Industries MBT Space Division, the MBT space satellites, and aspects of the AMOS 2 communications satellite project, including the launch process, deploying the satellite in space, and unique aspects of software development for satellite projects. The presentation will focus on the various environments in which the AMOS 2 software was tested, the nature of the tests, and the software measurement findings connected with the various aspects of these software testing efforts. Keyword-driven Testing (Abstract) Ayal Cohen & Tal Joseph, Mercury In this talk, the concepts of keyword-driven testing and business process testing are introduced. First the concepts are described theoretically, after which we demonstrate a real-world example that shows how these testing methods are being used by business analyst and automation engineers. The main benefit of the approach is that after the QA engineer creates testing assets and tests, subject matter experts can continue and create the bulk of their own tests. This approach has proved very useful for business process testing. Security Bulletins - Lessons Learnt, Changing the Way We Test Products and Patches (Abstract) John Neystadt, Microsoft Security patches are known to be a major customer pain. Business impact and installation costs are among the problematic factors, and as the Blaster and Slammer viruses proved, they may damage security more than they improve it. Industry is expected to build unbreakable products with service lifetimes of 10 years. How can this be done, with threats and attack technologies changing every 2-3 years?