Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: 23 Nov 93 15:47 -0800
From: Nancy Day <day@cs.ubc.ca>
To: info-hol <info-hol@cs.uidaho.edu>
Cc: day <day@cs.ubc.ca>
Message-Id: <3398*day@cs.ubc.ca>
Subject: UBC Tech Report available

The work I completed for my master's thesis on the  semantics  of
statecharts  and  a model checker is now available in a technical
report for anonymous ftp from ftp.cs.ubc.ca in /pub/pickup/day as
ubctr93-35.ps.Z.   The  abstract  follows at the end of this mes-
sage.

Accompanying files giving the HOL88 definitions  for  the  syntax
and  semantics  of  statecharts  and the model checking functions
along with some examples can be found in day_sc.tar.Z .  Since  I
use  the  Voss verification system to run my model checker, exam-
ples of running the model checker itself and some  special  tools
which  extract  variable  information from the textual statechart
are not included although they are described in the tech  report.
I am hoping to make it more portable in the coming months.

Any comments on this work would be most appreciated or if you are
interested  in  any  extensions I am working on to the semantics,
please send mail to day@cs.ubc.ca .

cheers, Nancy Day


               A Model Checker for Statecharts
           (Linking CASE tools with Formal Methods)
           ----------------------------------------

                University of British Columbia
                    Technical Report 93-35
                         October, 1993

Computer-Aided Software Engineering (CASE) tools encourage  users
to  codify  the specification for the design of a system early in
the development process.  They often  use  graphical  formalisms,
simulation,  and  prototyping to help express ideas concisely and
unambiguously.  Some tools provide little more than syntax check-
ing  of  the  specification  but  others  can  test the model for
reachability of conditions, nondeterminism, or deadlock.

Formal methods include powerful tools like automatic model check-
ing  to  exhaustively check a model against certain requirements.
Integrating formal techniques into the system development process
is  an  effective  method  of providing more thorough analysis of
specifications   than   conventional   approaches   employed   by
Computer-Aided  Software  Engineering  (CASE) tools.  In order to
create this link, the formalism used by the CASE tool must have a
precise  formal semantics that can be understood by the verifica-
tion tool.

The CASE tool STATEMATE makes use of an extended state transition
notation  called  statecharts.  We have formalized an operational
semantics for statecharts by embedding them in the logical frame-
work  of  an  interactive  proof-assistant  system called HOL.  A
software interface is provided to extract a  statechart  directly
from the STATEMATE database.

Using HOL in combination with Voss, a  binary  decision  diagram-
based  verification  tool,  we have developed a model checker for
statecharts which tests  whether  an  operational  specification,
given  by  a statechart, satisfies a descriptive specification of
the system requirements.  The model checking procedure is a  sim-
ple  higher-order  logic function which executes the semantics of
statecharts.

In this thesis, we describe the formal semantics  of  statecharts
and the model checking algorithm.  Various examples, including an
intersection with a traffic light and an arbiter,  are  presented
to illustrate the method.

This work was submitted in partial  fulfillment  of  requirements
for  a  Master  of  Science  degree  at the University of British
Columbia, September, 1993.

------------------------------------------------------------
Nancy Day, PhD student, CS, UBC, Vancouver, Canada
day@cs.ubc.ca