Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting

Testing and verification of asynchronously communicating objects in open environments are challenging due to non-determinism. We explore a formal approach for black-box testing by proposing an interface specification language that gives an assumption-commitment style description of an object's behavior. The approach is applied to Creol objects. Creol is a high-level, object-oriented modelling language, hence we do model-based testing of behavioral models. The testing is done by synchronising execution of a specification and the component under test. Due to the asynchronous nature of communication, testing should be done up-to observational equivalence. This leads to a large increase in the reachable state space for the test cases. We reduce the state space by using facilities for rewriting modulo AC (associativity and commutativity) built into the rewriting logic system Maude, and explore the state space by breadth first search. We present experimental results that show the usefulness of this approach.