Since 2014, MoMuT also provides support for Timed Automata test models via the stand-alone tool MoMuT::TA. Timed automata are among the most widely spread formalisms for specifying real-time behavior. They are finite state machines extended by real-valued clocks, which measure the passage of time. In classic timed automata time can only pass in locations. Invariants, linked to locations, are clock constraints restricting the amount of time that can be spent in these locations. Additionally, clocks can be used in the guards of transitions, to specify the time span during which the transitions are enabled. Each transition contains a (possibly empty) set of clocks that are reset when the transition is traversed. MoMuT::TA does not contain a graphical user interface for modelling the systems. Instead, modelling is done in the well-established timed automata tool UPPAAL and MoMuT::TA builds on the XML-structured files provided by the UPPAAL. Thus, the screenshots of the models presented here were also taken from UPPAAL and the models are processable by MoMuT::TA.
The figure to the left illustrates the same car alarm system that is also available in Action Systems Syntax and as UML state machines. The model contains four inputs that reflect the locking/unlocking and closing/opening of a cars doors. If the doors stay closed and locked for twenty seconds, the system is armed. This is an output of the system, usually indicated by a red blinking light. If the doors are opened after that, without being unlocked first, the alarm starts.
The main purpose of MoMuT::TA is the generation of test suits by applying model-based mutation testing. The current release provides two mutation operators: turning transitions into self-loops (thus, omitting the state-change) and changing transitions so that they lead to sink states (input-enabled locations, that can not be left and do not trigger any outputs). In a separate research branch seven additional mutation operators have been investigated, that will soon be incorporated into the next release. MoMuT::TA applies a tioco conformance check between the specification and the mutants. This conformance check is internally expressed as a language inclusion problem, and solved via the SMT solver Z3.
As the language inclusion problem can only be solved for non-deterministic observable transitions, MoMuT::TA also provides bounded determinization, where it unfolds an automaton (or a network of automata) and determinizes it on the fly. The figures below illustrate a simple coffee machine and an unfolded determinized version. The coffee machine takes a coin as input and either lets the user choose between coffee and tea, or refunds the coin after five seconds. The model is very abstract and does not specify the conditions (e.g. the system is not warmed up yet) for the different reaction to the coin. The unfolding was done up to depth three and the two transitions with coin label that leave the initial state were merged into one.
The current release of MoMuT::TA can be found in the Downloads section.
