Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Mon, 2 Mar 92 11:07:41 GMT
From: vac@uk.ac.cam.cl
Message-Id: <9203021107.AA05544@petrel.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted, kprasad@edu.caltech.cns
Subject: Re: HOL, Boyer-Moore or Stateharts


> I have a few requirement specifications that are expressed as
> Statecharts.  I am interested in knowing if HOL or the Boyer-Moore
> logic gives me any more functionality than Statecharts.

If by functionality you mean expressiveness, then I don't think you are going
to gain anything from going to higher order logic. You can add timing
constrains to Statecharts. (See Y. Kesten and A. Pnueli, Timed and Hybrid
Statecharts and their Textual Representation, Lect. Notes in Comp. Science,
vol. 571, Jan 1992)
You may be able to obtain a more accurate model by using h.o.l. by adding
more detail to your specification but you could do this with any language.

> For example, what value would I get if I migrated from Statecharts to
> using one of these theorem provers?


If you translate your Statecharts specification to h.o.l. you should be
able to show (by proof methods) some properties of the system. For example
reachability or the lack of, liveness, dead lock, mutual exclusion, etc.
This is not a trivial thing to do. From the Statecharts quadruple
(B,sigma,pi,E) you will end-up with a series of predicates and functions.
My guess is that they will need extensive support (by proving first some
lemmas) before you can get anything useful.

> Can I reason about the
> specifications better and make them more complete?

My understanding is that there are no supporting tools for reasoning in
Statecharts. You can test your specifications and probably do most of the
things you need with it?

> Right now, I feel that my specifications are "sort of" incomplete.

If your project is not top secret, I would be interested in looking at what
you are doing.

Victor. vac@cl.cam.ac.uk
        vac@air12.larc.nasa.gov