Atomic Action Refinement in Model Based Testing

In model based testing (MBT) test cases are derived from a specification of the system that we want to test. In general the specification is more abstract than the implementation. This may result in 1) test cases that are not executable, because their actions are too abstract (the implementation does not understand them); or 2) test cases that are incorrect, because the specification abstracts from relevant behavior. The standard approach to remedy this problem is to rewrite the specification by hand to the required level of detail and regenerate the test cases. This is error-prone and time consuming. Another approach is to do some translation during test execution. This solution has no basis in the theory of MBT. We propose a framework to add the required level of detail automatically to the abstract specification and/or abstract test cases. This paper focuses on general atomic action refinement. This means that an abstract action is replaced by more complex behavior (expressed as a labeled transition system). With general we mean that we impose as few restrictions as possible. Atomic means that the actions that are being refined behave as if they were atomic, i.e., no other actions are allowed to interfere.