Tuesday, 25 Apr. 2006, 17:00 (note the unusual weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Testing is one of the costliest aspects of commercial software development. Not only laborious and expensive, it also often lacks systematic engineering methodology, clear semantics and adequate tool support.
Model-based testing is one of the most promising approaches for addressing these deficits. At Microsoft, model-based testing technology developed by the Foundations of Software Engineering group in Microsoft Research has been used internally since 2003. The second generation of this tool set, SpecExplorer, deployed in 2004, is now used on a daily basis by Microsoft product groups for black-box testing of operating system components, .NET framework components and other areas.
SpecExplorer is a tool for testing reactive, object-oriented software systems. The inputs and outputs of such systems can be abstractly viewed as parameterized action labels, that is, as invocations of methods with dynamically created object instances and other complex data structures as parameters and return values. From the tester's perspective, the system under test is controlled by invoking methods on objects and other runtime values and monitored by observing invocations of other methods. The specification or the expected behavior is provided by a high level program called a model program that is written in the specification language Spec# or AsmL.
In this talk we give a brief introduction to the technology used in the SpecExplorer tool. For an easy read overview see [extended-abstract].
A detailed overview of the foundations of SpecExplorer can be found in MSR-TR-2005-59.