What is principal difference between FSM and LTS and what is the approach used by SpecExplorer? RRS feed

  • Question

  • During our literature study around MBT and MBT tools we found two important approaches used by MBT tools: Labelled Transition System (LTS) and Finite State Machine (FSM)

    What is the approach used by SpecExplorer? Is that LTS or FSM?

    Please can you provide some cons and pos of the two methods?


    Some MBT tools prefer LTS instead of FSM because of the following reasons:

    – LTS is a very basic model for describing system behavior.

    – LTS is more fundamental, more naive, and simpler, thus has better supports for the descriptions of non-determinacy, concurrency and composition

    – LTS can serve as underlying semantics model for much other formalism (e.g., FSM, EFSM, and timed models)

    – Restrictions on FSM (to enable driving the test executions): deterministic, completeness

    – FSM has always alternations between inputs and outputs

    – FSM is required to be ”deterministic” and ”complete” for testing

    – FSM is not compositional

    – Difficult to specify interleaving in FSM.

    What are the drives for SpecExporer to use LTS or FSM?


    We will introduce MBT as part of our testing approach. And we are now in tool selection phase. We have a the above open question around modeling principle used by different tool providers.

    I would appreciate if you could address (part of) these questions and help us to make decision for our tool selection.


    Best regards



    additional information:

    One of the sources we use in our study  is following:


    Model-Based Testing of Reactive Systems (Brian Nielsen)



    See also next slides

    FSM-test generation

    <button class="vspib"></button> - [ Vertaal deze pagina ]


    U heeft dit openbaar een +1 gegeven. Ongedaan maken

    Bestandsformaat: PDF/Adobe Acrobat - Snelle weergave
    FSM-test generation. Brian Nielsen bnielsen@cs.auc.dk. Department of Computer Science, ..... •Can be translated into FSM if variables have bounded domain ...



    • Edited by RachidP Saturday, September 17, 2011 11:51 AM
    Saturday, September 10, 2011 8:46 AM


  • Hi Rachid,

    The theoretical foundation of Spec Explorer is Action Machines (AMs). It's closer to Labeled Transition Systems than to Finites State Machines (in particular, it supports infinite state spaces). Some of the reasons why we picked AMs instead of FSMs are the ones in your list above: better support for concurrency, compositionality, non-determinism, etc. For an in-depth introduction to Action Machines, please take a look at our IJSEKE paper: http://academic.research.microsoft.com/Paper/2504135.aspx.

    If you don't have access to the journal, there's a similar version in the Technical Report here: http://research.microsoft.com/apps/pubs/default.aspx?id=70264.



    Thursday, September 22, 2011 11:16 PM