IEICE Trans - State Machines as Inductive Types

State Machines as Inductive Types

Kazuhiro OGATA
Kokichi FUTATSUGI

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Vol.E90-A No.12 pp.2985-2988
Publication Date: 2007/12/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e90-a.12.2985
Print ISSN: 0916-8508
Type of Manuscript: LETTER
Category: Concurrent Systems
Keyword:
Coq, formal methods, invariant properties, program specification, observational transition systems (OTSs),

Full Text: PDF>>

Summary:
We describe a way to write state machines inductively. The proposed method makes it possible to use the standard techniques for proving theorems on inductive types to verify that state machines satisfy invariant properties. A mutual exclusion protocol using a queue is used to exemplify the proposed method.