3rd Estonian Summer School in
Computer and Systems Science (ESSCaSS'04)

III Eesti Arvuti- ja Süsteemiteaduse Suvekool (EASTS'04)

SPECIFICATION AND BLACK-BOX TESTING OF SOFTWARE WITH SPEC#

Speaker: Margus Veanes
Microsoft Research, Redmond
http://research.microsoft.com/users/margus

Abstract:

Spec# is a specification language that extends C# with contracts and high-level data structures like sequences, sets and maps. Spec Explorer is a tool for exploring and validating specifications written in Spec# and AsmL, as well as using such specifications for advanced model-based testing of .Net applications. The main goal of the lectures is to teach about model-based testing, what it can do for you, and to introduce the underlying testing theory and algorithms used by the Spec Explorer tool. After the lectures one should be able to use the Spec# modeling language to describe testable behavior for both deterministic systems and for nondeterministic (multi-threaded or distributed) systems. During the course of the lectures we will look at various tasks related to model-based testing and development, such as, generating finite state machines from (possibly infinite-state) Spec# models, generating test cases for various test purposes, running the Spec Explorer tool to execute the generated test cases against a .Net implementation, and running the Spec Explorer tool on-the-fly (in stress-testing mode) against a .Net implementation.