A finite state machine (FSM) is a model for the state behavior of a system. Applying the FSM technology is very helpful for describing and manipulating software and hardware systems. The structure of the system becomes transparent by enumerating its states. The dynamics of the system are reflected by transitions from one state to another state. Figuring out the system's dynamics can be made easy by selecting a single state and focusing on the transitions leaving this state. A transition is accompanied by a trigger which is the cause of executing the transition. Actions can be defined for being processed during a transition. Actions can also be defined for the moments of entering or leaving a state. Furthermore, finite state machines include advanced features like superstates, substate machines, pseudo-states, orthogonal states, etc. A system may contain dozens of FSMs which interact with each other in a synchronous or asynchronous way. Proving the correctness of a whole system manually will be difficult in case of many FSMs. Tool support is needed to verify the modeled FSMs automatically.

TismTool is a relatively new tool with a set of unique features for handling FSMs including verification. The philosophy of the TismTool methodology is elaborated in a whitepaper. TismTool is designed by a software engineer who knows very well the tricks of software development. The workflow of TismTool fits a software development process in a natural way. Common UML diagrams serve as the input for the tool. The applied diagrams are composite structure diagrams, class diagrams, and of course state machine diagrams. Software developers are familiar with these UML diagrams from classes at university or from daily practice. A recipe is provided how to model the interrelated UML diagrams. The diagrams are useful for structuring your thoughts and documenting the system on behalf of maintenance. But most important is that consistent source code can be generated from the diagrams in the popular programming languages C, C++, Java, and C# . The generated source code has two main objectives. Firstly, the generated code can be part of your final system’s application. Secondly, the source code can be used for the verification of the modeled system. The generated source code for the application and the code for the verification are almost the same. The verification source code contains only additional statements for logging visited states and transitions. The big advantage of this methodology is that all statements of the delivered application source code have been executed during the verification.

The workflow of the verification consists of two phases. In the first phase, the Protocol State Machines of the interfaces are verified. In the second phase, the FSMs of the components’ implementations are verified. TismTool is capable of verifying an arbitrary subsystem of components as a whole. It is important to verify two or more components together to avoid that deadlock situations would be left unnoticed. That could happen if components are only verified individually as shown in pitfalls (in Dutch).

Another beneficial feature of the TismTool methodology is the possibility to include programming statements in the actions according to the target programming language (C, C++, Java, C# ). The actions in a model may contain manipulations of variables defined in the FSM’s class object, while loops, library calls, even system calls, etc. This will save a lot of effort, since there is no need any more to design artificial foreign components with trivial statements. An additional advantage is that the included statements are executed during verification. That would not be the case for mocked foreign components. In fact the TismTool methodology advocates the platform specific model (PSM) approach opposed to the platform independent model (PIM) approach, refer to the comparison about model verification. Most systems require only a single target programming language. Still, code generation for more than one programming language can be realized in TismTool by the (optional) translation tables for code phrases. Hence, all these facilities in TismTool allow a way of working that is much closer to what a software engineer is used to.

The productivity of the software development is highly increased thanks to the source code generation and verification. The Run-Time Environment (RTE) of TismTool takes care of thread management and semaphore management. Components in a software architecture can be modeled for having a thread. The RTE provides thread creation, marshalling data, queue management and rendez-vous notification. These well-established interprocess communication mechanisms relieve the software engineer from implementing such tedious and error prone services. The execution environment inside a thread automatically protects data against concurrent access. Multiple components inside a super-component may share the same thread so that overhead of task switching is decreased. TismTool offers a second protection mechanism that is based on a mutex. Usage of one of both mechanisms is at the choice of the developer. In the case of absence of concurrent access no protection will be needed leading to improved performance. Guidelines about these choices are given by the web-based TismTool documentation. Also, many examples are available.

TismTool is free of charge, at least for the time being! So, enjoy visiting the website www.tismtool.com.

Protocol State Machine (client role)

Protocol State Machine (server role)

Finite State Machine