Naval Postgraduate School, Monterey, and
, Inc., Cupertino, California, USA
Semantics and Runtime Monitoring of TLCharts:
Statechart Automata with Temporal Logic Conditioned Transitions.
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.
Redmond, Washington, USA
Specifying and Testing Software Components with SpeC#
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.