locked
Questions about the "State" concept RRS feed

  • Question

  • Hi,

    I have used spec-explorer for quite a while, and created a few simple instance-based modeling solutions. I think it helps to model the system under inspection with system constraint and process constraint and parameter domain constraint.

    Is there a "State" concept or a similar one in spec-explorer? I have a few questions about the "State".

    Question 1: What is "State" space for a instance-based modeling solution? All combinations of member variables of instances and interactions between instances?
    Question 2: In the exploration graph, what does the diamond-shaped one mean?
    Question 3: What is the behavior expression denoted by the "Construct model program from ConfigName"?
    Question 4: During a machine exploration(attached to a model program), how are instance variables filled? It seems that spec-explorer generates  them for my test cases. But if I want to run test cases without spec-explorer, anything else should I do?

    Thanks in advance


    • Edited by lzh_ing Tuesday, August 28, 2012 3:10 PM
    Tuesday, August 28, 2012 3:09 PM

Answers

  • Hi Lzh_ing,

    To 1/3 and the state concept:
    Spec Explores uses "Guarded State Update Rules" to model systems.
    The concept should be equivalent to state machines (FSM or eFSM - see page 47 of the book of Lee and Seshia):
    It is quite simple to imitate FSM's with Spec Explorer.

    FSM:
    * A transition in an FSM consists of a guard and an "action". The guard is controlling these "actions".

    Spec Explorer:
    * The Spec Explorer rules are equivalent to these FSM-transitions.
    Rules are guarded by constraints (Condition.IsTrue). And the rest of the rule-body is the similar to the FSM-"action".

    Hand-Waving I would say: The main difference is that by default in Spec Explorer the rules are allowed in all states. 
    You have to explicitly restrict the rules using the guards.
    In contrast in an FSM by default states have to be explicitly connected with transistions to allow a new transition from/to a state.

    To your questions: The "state space" is the fully explored machine.
    So it is the combination of all allowed instances and their member variables which can be reached using the allowed rules.
    Generating the exploration from the FSM or Guarded State Update Rules is not trivial:
    E.g. you can model hierarchical eFSM's connected in a parallel or serial setup (composition).

    To 2: The diamond is showing non-determinism: one or more transitions from this state are e.g. driven from the SUT via events.
    Lee and Seshia do not use the diamond, but red-coloured transitions to mark this.

    To 4: The state content is not needed and intentionally hidden for the test cases. See posting of Nico on http://social.msdn.microsoft.com/Forums/de-DE/specexplorer/thread/89583a26-0cbf-4044-831d-c2ce86913b06:

    • Marked as answer by lzh_ing Tuesday, September 11, 2012 3:24 PM
    Monday, September 10, 2012 2:43 PM

All replies

  • Hi Lzh_ing,

    To 1/3 and the state concept:
    Spec Explores uses "Guarded State Update Rules" to model systems.
    The concept should be equivalent to state machines (FSM or eFSM - see page 47 of the book of Lee and Seshia):
    It is quite simple to imitate FSM's with Spec Explorer.

    FSM:
    * A transition in an FSM consists of a guard and an "action". The guard is controlling these "actions".

    Spec Explorer:
    * The Spec Explorer rules are equivalent to these FSM-transitions.
    Rules are guarded by constraints (Condition.IsTrue). And the rest of the rule-body is the similar to the FSM-"action".

    Hand-Waving I would say: The main difference is that by default in Spec Explorer the rules are allowed in all states. 
    You have to explicitly restrict the rules using the guards.
    In contrast in an FSM by default states have to be explicitly connected with transistions to allow a new transition from/to a state.

    To your questions: The "state space" is the fully explored machine.
    So it is the combination of all allowed instances and their member variables which can be reached using the allowed rules.
    Generating the exploration from the FSM or Guarded State Update Rules is not trivial:
    E.g. you can model hierarchical eFSM's connected in a parallel or serial setup (composition).

    To 2: The diamond is showing non-determinism: one or more transitions from this state are e.g. driven from the SUT via events.
    Lee and Seshia do not use the diamond, but red-coloured transitions to mark this.

    To 4: The state content is not needed and intentionally hidden for the test cases. See posting of Nico on http://social.msdn.microsoft.com/Forums/de-DE/specexplorer/thread/89583a26-0cbf-4044-831d-c2ce86913b06:

    • Marked as answer by lzh_ing Tuesday, September 11, 2012 3:24 PM
    Monday, September 10, 2012 2:43 PM
  • Hi Bububu,

    Thanks for your kind reply.

    I think Spec-explorer is a practical framework to modelling a system, and I feel it works in the following manner.

    In a certain exploration step, the spec-explorer exhausts all rule methods to figure out next step within the state space restricted by parameter constraint and  the "Condition.In() constraint and behavior expressions.

    To Question 3: 

    What is the behavior expression denoted by the "Construct model program from ConfigName"?

    I feel like it tries to figure out a route which covers all the rule methods as few as possible, is that right?  

    Thanks in Advance.

    Lzh_ing

    Tuesday, September 11, 2012 3:40 PM
  • Hi Lzh_ing,

    concerning the expression "Construct model program from ConfigName", I think your explanation for exploration is decribing it well.
    With this expression the behavior of the model program is generated.
    I think here the behavior is the sum of all allowed steps and their sequence and states of the model.
    "As few as possible" is true in a sense that every state and step is unique in this behvior: it is the state machine (this is why I tried to compare Spec Explorer with state machines).

    Hope this helps somehow

    Wednesday, September 12, 2012 8:35 AM