PROSPER AT Edinburgh

Proof and Specification Assisted Design Environments

Model checking with English specifications

Here is a circuit for a single pulser. This circuit converts each finite duration input pulse (signal "i") into a unit duration output pulse (signal "o").

You can attempt to specify the behaviour of this circuit using an English sentence. The sentence will be translated into the temporal logic CTL and passed to the model checker program SMV. You should use the names "sigi" and "sigo" to refer to the two signals (and if you wish, "sigx" and "sigy" for the two intermediate signals).


Either select an example:

After sigi is false after sigi is true sigo is true.
(two CTL interpretations, both false)
If sigi is high then sigo is low
(one, true interpretation)

...or type in your own sentence:


This system makes use of the Alvey Natural Language Tools.

25 November 1999