Skip to content

Design decisions for the formalization of hFSMs

Jump to bottom
Alberto Tacchella edited this page Sep 4, 2018 · 9 revisions

This page is concerned with the definition of the hFSM data type.

Existing approaches

Many projects have already modelled various kinds of FSMs into Coq.

coq-contribs

Here is a list of relevant-looking projects from the directory of "user-contributed libraries" in Coq:

  • coq-automata (written in 1993)

    Relevant files are: Reg.v (~1500 lines, defines FSM, eFSM). Imports:

    • Ensf.v (an implementation of finite sets as lists)
    • Max.v
    • Words.v (words and languages)
    • Dec.v (definition of subset by separation with a predicate)

  • p-automata (written in 2001)

    Formalizes "parameterized automata". Relevant files are:

    • Transitions
    • Time, TimeSyntax, Timebase
    • PAutomata, PAuto

    (see also Paulin-Mohring in Kobayashi, Pierce (eds), p.309)

  • coq-fairisle (written in 2005)

    "Moore and Mealy automata are co-inductively axiomatized and are used to uniformly represent both the structures and the behaviours of circuits."

Formalization of UML Statecharts by Sheng, Dou, Yang

This paper looks very relevant. They start from a small-step operational semantics given by von der Beeck in 2002. Code is available.

Starting from scratch

However, our best option is probably to start from scratch and develop a completely new implementation.

One of the reasons to do this is the following. In order to proceed with the automatic extraction of a workable specification of the FSM (to be fed into the NuSmv model checker), we need our "FSM" datatype to mirror as closely as possible the way in which a FSM is specified in the SMV language. None of the above implementations fares well in this respect. Moreover the implementations in coq/contrib are (typically) purely declarative, i.e. they model a transition relation as a term of type States -> States -> Prop. These terms do not survive program extraction, so from our perspective this approach is useless.

For us it is more natural to model a transition relation as an element of an inductive type which is built in a "step by step" way by adding transitions, in a manner which parallels the way a FSM is specified in SMV (namely: state space described by variables on finite sets, transitions specified by invariants and next assignments, epsilon-transitions specified by define statements).

In this way it should be feasible to mechanically translate an element of this datatype into a NuSmv specification (that actually uses a very restricted subset of the smv language).

Clone this wiki locally