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

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

Pedase, August 8-12, 2004.


Speaker: Margus Veanes
Microsoft Research, Redmond


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.


Valid CSS! Valid XHTML 1.0 Strict Last modified on August 05 2004 21:39:41. esscass04 at cc.ioc.ee