verification of real-time specs

[Thomas Weigert]

I was wondering if the following two tools are either in the public domain,
or available for a reasonable (reasonable in terms of university funding)
license fee:

(1) EMC
(2) AUTO

EMC is a model checker for CTL formulae over Kripke structures. Literature:
Emerson, Halper, "Sometimes" and "Not Never" Revisited, JACM, 33, 1, 1986.

AUTO converts CCS specifications into transition systems. Literature: de
Simone, Vergamini, Aboard AUTO, I.N.R.I.A. Tech. Rep. 111, 1990.

I would also appreciate pointers to other similar tools.

Cheers, Thomas.

--
+--------------------------------+---------------------------------+
| Thomas Weigert | |
| Machine Inference Section | |
| Electrotechnical Laboratory | |
| Umezono 1-1-4, Tukuba-shi | weigert@{mcs.anl.gov,etl.go.jp} |
| Ibaraki 305, Japan | +81-298-58-5918 (phone+fax) |
+--------------------------------+---------------------------------+

[Thomas Weigert]

In a recent post, I wrote

TW> EMC is a model checker for CTL formulae over Kripke structures.
TW> Literature: Emerson, Halper, "Sometimes" and "Not Never" Revisited,
TW> JACM, 33, 1, 1986.

It was brought to my attention that above statement could be construed as
claiming that the mentioned paper was the seminal reference about the EMC
system or model checking. Of course, it is not, but it was the only
reference that mentioned model checking at the time of posting. Model
checking was first proposed by E.M. Clarke.

Probably the best reference for EMC is E.M. Clarke, E.A. Emerson, A.P.
Sistla, "Automatic Verification of Finite-State Concurrent Systems Using
Temporal Logic Specifications", ACM Trans. Programming Languages and
Systems, 8, 2, 1986, pp. 244-263.

I apologize for any confusion my post might have caused.