Axini develops tools for model based testing (MBT) and model based software engineering (MBSE). Model based testing is a software testing approach in which test cases are automatically generated and executed from a model, a formal specification of the system under test. This approach allows for a high degree of test automation and more thorough testing.
Models may consist of multiple parallel processes. When two of these processes need to synchronize, they can use an internal message for communication. This synchronization is like a handshake agreement: both processes must complete the handshake before continuing. Failure to complete the handshake can sometimes result in a deadlock, causing the test run to stop.
This makes internal synchronization a vital part of the model to get right. However, it can be challenging to debug.
The difficulty of internal communication is that the internal messages are not visible to the modeler; they do not appear in test results. It is therefore hard to analyze which internal synchronizations did or did not occur.
Furthermore, the explorer tool, which can be used to traverse through models, hides internal communication. The model visualization also does not show internal messages as synchronization pairs.
Possible research questions
There are several puzzles and research questions that students can work on.
How can we effectively display internal communication in test results?
How can we improve the explorer to allow effective debugging of internal communication?
How can concepts such as parallelism or non-determinism be visualized effectively?