Invited Speakers

Doron Drusinsky
Naval Postgraduate School, Monterey, and
Time Rover , Inc., Cupertino, California, USA

Title: Semantics and Runtime Monitoring of TLCharts:
Statechart Automata with Temporal Logic Conditioned Transitions.

Abstract: This talk describes the semi-formal semantics and a run-time monitoring technique for TLCharts, a visual specification language that combines the visual and intuitive appeal of non-deterministic Harel Statecharts with formal specifications written in Linear-time (Metric) Temporal Logic (LTL and MTL). We describe an automata-theoretic semantics for non deterministic statecharts with negation and state overlapping and extend it to cater for temporally annotated transitions, thereby providing a simple automata theoretic semantics for TLCharts. We also describe a run-time monitoring technique for TLCharts.

Wolfram Schulte
Microsoft Research
Redmond, Washington, USA
Personal website

Title: Specifying and Testing Software Components with SpeC#

Abstract: SpeC# is a formal language for API contracts, based on Asml (a wide spectrum formal specification language), which extends C# with constructs for preconditions, postconditions, object invariants, and model programs (behavioral contracts that take the history of the entire run into account). Spec# is the input to a suite of correctness tools. These tools include static and dynamic verification, a test case generator and a model checker. Our goal is that Microsoft product teams will be able to write SpeC# contracts as simply or richly as they like and then drive all of their checking tools from this common contract. In this talk I will discuss SpeC# and its use for testing. Our SpecExplorer tool provides a rigorous, systematic way to generate behavioral test cases. With SpecExplorer testers can search the space of all possible sequences of method invocations that 1) do not violate the pre- and postconditions of the system's contracts and 2) are relevant to a user-specified set of test properties. The resulting traces are algorithmically traversed to produce behavioral tests that cover all explored transitions. SpeC#'s Runtime Conformance Checker is used for test verification. It uses a specially instrumented build to dynamically enforce contractual constraints that cannot be statically verified. More than just "assertion checking" familiar to all programmers, the conformance tool handles nondeterministic actions (such as user input and the handling of events) and the mapping of abstract state given in an interface's contract with concrete state defined by the implementer.


Doron Drusinsky, B.Sc. 1983, Technion, Haifa, Israel, Ph.D. 1988, Weizmann Inst., Israel., Gad Reshef award. From 1988-1992 Doron worked for Sony corp., where he developed a novel (for its time) hardware synthesis application and participated in one of the first commercial digital cell phone voice compression projects. In 1993, Doron established R-Active Concepts, Inc., a provider of high-level development tools for embedded systems market; in this capacity Doron designed the first efficient code generator for Harel statecharts. These tools were acquired by ISI, now part of Wind River Systems, in 1997. In 1998 Doron developed the Temporal Rover, one of the first run-time monitoring tools, currently used by NASA JPL. From 2000 to 2002 Doron participated in the development of a wide area low cost sensor system at Xerox PARC. Doron is currently the president and CTO of Time Rover Inc. and also an associate professor of computer science at the Naval Postgraduate School in Monterey where his primary interests are run-time monitoring and light-weight verification methods for embedded systems.

Wolfram Schulte is a member of the Foundations of Software Engineering (FSE) group at Microsoft Research in Redmond, Washington. He currently leads a research project focused on advanced technologies for software modeling and verification. Wolfram has also interest in programming language design and implementation. During recent years he researched data access integration and in particular how to combine SQL and XML with C#. Wolfram has published a variety of papers in the areas of language design, model-based testing, verification, program derivation and compilation. Before joining Microsoft Research in 1999, Wolfram was assistant professor for computer science at the University of Ulm, where he received his "habilitation" (second PhD) and at the Technical University Berlin where he got his first PhD. He also worked as project manager for a German software company.