Attack-driven Test Case Generation Approach using Model-checking Technique for Collaborating Systems

The formal verification technique of model-checking can be used to derive test cases. This approach has become popular as it provides the capabilities of exhaustively exploring the state space of the modeled system and generates counterexamples for properties specified over the model. However, counterexamples only show states, transitions and the values of their parameters. In addition, its semantics are also dependent on input model specification languages and trace representation notations. In this paper, we present a focused test case generation approach from PAT model checker for collaborating systems. The focus is driven by specific and putative attack behaviours. To this end, we devised test specification rules/algorithm to translate counterexamples to lest cases. The translation aims at reducing semantic gaps between counterexamples and the corresponding test cases. We assess the viability of the test cases generated from our approach by using JADE simulation framework for aircraft landing scenario in air traffic control domain.