SOTA 2011

Workshop on the State of the Art in Automated Software Engineering Research

Co-located with the ASE PC meeting

Date: July 11, 2011 (Monday), the day before the PC meeting

Venue: NASA Ames Conference Center (the same as the PC meeting)
The workshop will be in Mezzanine (and the PC meeting in Showroom).
Everybody will need to show an id at the gate and say they go to this meeting in Building 3.

Program: 25-minute slots (20 for talk, 5 for questions), 30-minute breaks and a 60-minute lunch
9:20-9:35 Introduction
9:35-11:15 Session on Cloud and Coordination
11:15-11:45 Break
11:45-1:00 Session on Testing I
1:00-2:00 Lunch
2:00-3:15 Session on Logic
3:15-3:45 Break
3:45-5:00 Session on Testing II


Capture Calculus

Presenter: Robert J. Hall
Abstract: Distributed embedded systems, such as multi-player smartphone games, training instrumentation systems, and ``smart'' homes, naturally have complex functional and non-functional requirements.  These are difficult to elicit, represent, validate, and verify. For high confidence, one demands that the represented requirements reflect realistic usage of the system; however, such usages, often representing human actions in complex environments, can have hundreds to thousands of steps and be impractical to elicit and manage using only declarative or intensional (computed) representations. Non-functional requirements like scalability increase this complexity further. In this talk, I show how one can bootstrap requirements using data captured from initial prototypes deployed in small scale real world tests.  Using such captures as seeds, I show how a calculus of transformations on captures, from captures to scenarios, among scenarios, and from scenarios back to captures can be used in several requirements engineering tasks.

TouchStudio: Programming on the Phone and Sharing Scripts in the Cloud

Presenter: Nikolai Tillmann
Abstract: TBA

Automated Software Engineering Research Issues in Cloud Computing

Presenter: Anna Liu
Abstract: TBA

Coordination Support in Software Development

Presenter: Anita Sarma
Abstract: TBA

Automated testing meets end-user programmers

Presenter: Margaret Burnett
Abstract: Automated forms of testing have been shown to improve validation productivity for software development as it is done by professional programmers. Still, recent government statistics have shown that professional programmers are but a small fraction of the people who develop software.

In this talk, we discuss, from a "people" perspective, the challenges in bringing automated forms of systematic testing to another, larger fraction of the people who engage in software development, namely end-user programmers. We then look at testing tools for end users in several testing settings, and discuss empirical studies of ordinary end users using these tools.

This is joint work with Alex Groce, Gregg Rothermel, Marc Fisher, Simone Stumpf, Weng-Keen Wong, Curtis Cook, and our students.

Enhancing Structural Software Coverage by Incrementally Computing Branch Executability

Presenter: Giovanni Denaro
Abstract: Structural code coverage criteria have been studied since the early seventies, and now they are well supported by commercial and open source tools. However, the industrial value of the structural criteria is limited by the difficulty of manually achieving high coverage scores, due to both the complexity of deriving test cases that execute specific uncovered elements and the presence of many infeasible elements in the code. In this work, we propose a technique that aims to increase branch coverage (possibly up to closely approximate 100% coverage), by both generating test cases that execute yet uncovered branches and identifying infeasible branches that can be eliminated from the coverage domain. The algorithm combines concolic testing, abstraction refinement, and a novel technique named coarsening, to execute unexplored branches, identify infeasible ones, and mitigate the state space explosion problem. This talk will present a set of experimental results obtained with a prototype implementation.

This is joint work with Mauro Baluda, Pietro Braione and Mauro Pezzè (to appear in Software Quality Journal 2011)

Optimized Delta Execution for Efficient Mutation Testing

Presenter: Marcelo d'Amorim
Abstract: Mutation testing regained significant force recently as a technique to assess the quality of a test suite.  One practical problem of mutation testing is the high cost associated with the execution of test cases.  This cost is proportional to the product of the number of test cases and the number of mutants; the later grows with the size of the application.  Despite the significant advances in reducing this cost it is still very high.  Recent experimental data indicates that mutation analysis of large applications can take hours even for test suites that run in seconds.  This talk will present the idea of using Delta Execution (DE) to optimize Mutation Testing and the recent optimizations in our DE implementation to enable this idea.  Conceptually, DE makes it possible to execute a test on all mutants, simultaneously.  For that it uses a special representation of state that explicitly encodes set of individual states.  Each individual state corresponds to a distinct mutant.  To make this idea practical we implemented optimizations of DE to explore parallelism and native execution.

This is joint work with Thiago Vieira.

Using SMT Solvers in the Context of ASE

Presenter: Nikolaj Bjorner
Abstract: TBA

Matching Logic: A New Program Verification Approach

Presenter: Grigore Rosu
Abstract: Matching logic is a new program verification logic, which builds upon operational semantics. Matching logic specifications are constrained symbolic program configurations, called patterns, which can be matched by concrete configurations. By building upon an operational semantics of the language and allowing specifications to directly refer to the structure of the configuration, matching logic has at least three benefits: (1) One's familiarity with the formalism reduces to one's familiarity with the operational semantics of the language, that is, with the language itself; (2) The verification process proceeds the same way as the program execution, making debugging failed proof attempts manageable because one can always see the "current configuration" and "what went wrong", same like in a debugger; and (3) Nothing is lost in translation, that is, there is no gap between the language itself and its verifier. Moreover, direct access to the structure of the configuration facilitates defining sub-patterns that one may reason about, such as disjoint lists or trees in the heap, as well as supporting framing in various components of the configuration at no additional costs.

CSSL: A Logic for Specifying Conditional Scenarios

Presenter: Arie Gurfinkel
Abstract: Scenarios and use cases are popular means of describing the intended system behaviour. They support a variety of features and, notably, allow for two different interpretations: existential and universal. These modalities allow a progressive shift from examples to general rules about the expected system behaviour. The combination of  modalities in a scenario-based specification poses technical challenges when automated reasoning is to be provided. In particular, the use of conditional existential scenarios, of which use cases with preconditions are a common example, require reasoning in branching time. Yet, formally grounded approaches to requirements engineering and industrial verification approaches shy away from branching-time logics due to their relatively unintuitive semantics.

In this work, we define an extension of an (industry standard) linear-time logic PSL with sufficient branching expressiveness to allow capturing conditional existential statements. The resulting logic, called CSSL (Conditional Scenario Specification Language), has an efficient model-checking procedure. It supports reasoning about heterogeneous requirements specifications that include universal and existential statements in the form of use cases and conditional existential scenarios, and other sequence chart variants, in addition to general (linear) liveness and safety properties. We report on two industrial case studies in which the logic was used to specify and verify scenarios and properties.

This is joint work with Shoham Ben-David, Marsha Chechik, and Sebastian Uchitel (to appear in ESEC/FSE 2011)

Automated GUI Interaction Testing: Incorporating Event Context

Presenter: Myra Cohen
Abstract: Automating system testing for programs with Graphical User Interfaces (GUIs) presents many challenges for the tester. There are an enormous and potentially unbounded number of ways to interact with the software under test, and test generation techniques need to adequately cover this interaction space. In this talk we present some recent work on a family of model-based GUI coverage criteria grounded in combinatorial interaction testing that consider context in terms of event combinations, sequence length, and absolute positions. We show the results of a study exploring the difference in effectiveness and cost of these new criteria. We then present an overview of some challenges and potential solutions for automatically achieving this coverage in practice.

This is joint work with Atif Memon, Xun Yuan and Si Huang

Cooperative Testing and Analysis: How Human and Machine Cooperate to Get Job Done

Presenter: Tao Xie
Abstract: Tool automation to reduce manual effort has been an active research area in various subfields of software engineering such as developer testing (where developers test their code as they write it). Manual developer testing is often tedious and insufficient. Then testing tools can be used to enable economical use of resources by reducing manual effort. To maximize the value of developer testing, effective and efficient support for cooperation between developers and tools is greatly needed and yet lacking in state-of-the-art research and practice. In particular, developer testing practice is in a great need of (1) effective ways for developers to communicate their testing goals and guidance to tools and (2) techniques and tools with strong enough capabilities to accomplish the given testing goals -- enabling a feedback loop between developers and tools to refine and accomplish the testing goals. A new research frontier on synergistic cooperation between developers and tools is yet to be explored. We have recently proposed the methodology of cooperative developer testing. This talk presents two recent advances towards cooperative developer testing. The first one (described in our ICSE 2011 paper) is on precisely identifying and reporting problems that prevent test-generation tools from achieving high structural coverage, in order to reduce the efforts of developers in providing guidance to the tools. The second one is on engineering an automated testing tool for serious games in computer science (, in order to help users (e.g., K-12 and  undergraduate students) to learn critical computer science skills such as problem solving skills and abstraction skills. Major work described in this talk is joint work with Xusheng Xiao from North Carolina State University, and Nikolai Tillmann and Jonathan de Halleux from Microsoft Research.

IMUnit: Improved Multithreaded Unit Testing

Presenter: Darko Marinov
Abstract: Multithreaded code is getting increasingly important but remains extremely hard to develop and test. Most recent research on testing multithreaded code focuses solely on finding bugs in one given version of code. While there are many promising results, the tools are fairly slow because they explore a large number of thread schedules and do not exploit the fact that code evolves through several versions during development and maintenance. Our overarching goal is to improve (regression) testing of multithreaded code.

This talk focuses on a novel approach to specifying and executing schedules for multithreaded tests. Traditionally, developers enforce a particular schedule with time delays, e.g., using Thread.sleep in Java. Unfortunately, this sleep-based approach can produce false positives or negatives, and can result in unnecessarily long testing time. We introduce a new language that allows specifying schedules as constraints on the events during test execution. We provide a tool that automatically controls the code to execute the specified schedule and a tool that helps developers to migrate their legacy, sleep-based tests into event-based tests in our language. The latter tool uses new techniques for inferring events and schedules from the executions of sleep-based tests. We describe our experience in migrating over 200 tests. The inference techniques have high precision and recall, of over 75%, and our approach reduces testing time compared to sleep-based tests, on average over 3X.

This is joint work with Milos Gligoric, Vilas Jagannath, Dongyun Jin, Qingzhou Luo, and Grigore Rosu (to appear in ESEC/FSE 2011)

Organizers for SOTA 2011:
  • Corina Pasareanu, Nasa AMES (ASE PC co-chair)
  • John Hosking, University of Auckland (ASE PC co-chair)
  • Darko Marinov, University of Illinois at Urbana-Champaign (helping with SOTA)

Previous related workshops: 2010 2009 2007