| Q: | Does TismTool leverage formal verification? |
| A: | No, formal verification requires applying formal methods or mathematics. Also, TismTool does not use formal specification languages, like CSP. |
| Q: | What are the (dis)advantages of TismTool compared to formal verification techniques? |
| A: | A comparison between the 2 techniques formal verification and runtime verification has been made in the paper comparison_fv_erv.pdf. |
| Q: | How does TismTool contribute to state machine verification? |
| A: | TismTool itself does not execute any verification, it only generates source code that will do the job. That generated code must be compiled, linked and executed in the target environment for yielding verification feedback. |
| Q: | What is the algorithm for the state machine verification? |
| A: | The algorithm is a brute force method of constructing all possible execution scenarios. The driving forces for the scenarios are native triggers. Duplication of scenarios is detected by comparing state machine configurations and queued messages. |
| Q: | Are native triggers the same as stimuli? |
| A: | No, there is a subtle difference. The effect of a native trigger is executing its activity being source code, that can hence contain any number of stimuli. |
| Q: | Can TismTool guarantee defect-free source code after successful verification? |
| A: | TismTool generates source code being free from the kind of defects analysed during verification: deadlocks, livelocks, queue overflows, rendez-vous synchronisation errors, unhandled functions, unvisited states, unvisited transitions. |
| Q: | Can TismTool guarantee fully defect-free source code after successful verification? |
| A: | No, nor can any other state machine verifier tool ! Defects caused by human mistakes violating the system's intended behaviour can never be detected by a computer program. |
| Q: | Could you give some counter examples? |
| A: |
The state machine of the airco software controller
checks (in CoolingSubFsm/Composite/choice-state) whether the current
temperature is less than or equal to a target temperature. A developer
might make a mistake and replace inadvertently the inequality by a
greater-than sign with the result of swapping 2 state transitions. A
verifier tool can not master the logic of an airco, and hence will not
report such a mistake. Furthermore, the airco system requires a hysteresis to prevent that the cooler will repetitively start and stop due to very slight fluctuations around the target temperature. For this reason the sensor is asked to signal if the temperature is below Target-1 (in CoolingSubFsm/Composite/Coolong) during cooling. Suppose, a developer implemented the hysteresis wrongly by entering the parameter Target+1. Such a simple mistake can never be detected by the verifier. Also, mistakes can creep in actions of state transitions, e.g., in controlling state machines of lower level components. An event DoLeft invoking the action pDriver->ExecRight() seems to be a bug, but for pragmatic reasons an unplanned swap of 2 hardware wires has been 'solved' in the controller's state machine. The verification will (rightly) detect no defects in this state machine, nor in the protocol between controller and driver. If the wires are corrected in the next system release without adjusting the controller, then again the verifier will not complain. |