Unifying modal interface theories and compositional input/output conformance testing

摘要

We present a novel formal foundation for model-based testing of component-based software systems, unifying principles from modal interface theories and input/output conformance testing. Our theory relies on Modal Interface Automata with Input Refusals (IR-MIA) as behavioral formalism for both the specification and the implementation under test. IR-MIA models allow for a fine-grained distinction between mandatory and optional, as well as between underspecified and forbidden input/output behaviors, thus improving expressiveness of existing approaches in various ways. The input/output conformance relation on IR-MIA, called modal-irioco, therefore supports positive and negative conformance testing with optimistic and pessimistic environmental assumptions and is preserved under modal refinement. Our theory further adapts a variety of different composition operators from interfaces theories to IR-MIA models, each enjoying-under moderate restrictions-desirable compositionality properties with respect to the modalirioco relation. Those operators include interface conjunction for incrementally integrating multiple perspectives on the same component, as well as parallel composition with multicast and hiding for integrating multiple concurrently interacting components. Furthermore, a quotient operator on IR-MIA, serving as the inverse to parallel composition, facilitates decomposition of conformance testing, thus providing a solution to the unknown-component problem. (C) 2018 Elsevier B.V. All rights reserved.