Technical accomplishments:  Work continued on the application
of Abstract State Machines (ASMs) to defining the operational semantics
of Stateflow. We have formally specified approximately 40% of an
abstract stack-based machine for evaluating Stateflow diagrams.

Verifying the generators is a key aspect of the project. We have
settled on using bisimulation (observational equivalence) as the
notion of correctness for the generators. That is, the translation
from the source to the target language is correct when the program
and its translations are observationally equivalent with respect
to the operational semantics of the two languages. Observational equivalence
has been made precise in the concurrency theory literature.

Internal publications:  A draft document has been prepared showing
the use of Specware specifications in higher-order logic to
capture the static semantics of Stateflow and a fragment of the
dynamic semantics.

Meetings: None.

Travel:  John Anton and Lindsay Errington attended the MoBIES PI meeting
in New Orleans, Jan 23 - 25, 2001.