State-machines in Coq

Question

Can I use Coq to prove that a state machine cannot reach an invalid state? How?

Answer 1

Here is how to translate stm from here to Coq.

Require Import Coq.Lists.List.                                                                                                                                                                

Inductive alpha : Set := A | B | C | D.

Fixpoint s1 (xs : list alpha) : bool :=
  match xs with
    | C :: rest => s2 rest
    | _ => false
  end

with s2 (xs : list alpha) : bool :=
  match xs with
    | nil => true
    | A :: rest => s2 rest
    | B :: rest => s2 rest
    | C :: rest => s3 rest
    | _ => false
  end

with s3 (xs : list alpha) : bool :=
  match xs with
    | D :: rest => s2 rest
    | _ => false
  end.

Here is the theorem stating that STM can't reach invalid state:

Theorem t : forall xs, s1 xs = false.

But obviously it is not true for this STM. In general case it could be proved by induction.

It will be easier to help you if you provide some more information on what is your actual state machine.

Answer 2

This seems more a question for a model checker than for a theorem prover.

There has been the question Can Coq be used (easily) as a model checker? about this, and there indeed is some work about using Coq as a model checker, see for example https://github.com/coq-contribs/smc, but it is probably not easy to use this for what you want to do.