PAT 기반 반례로부터 테스트 시퀀스로의 체계적 변환

Abstract

Model checking approach has become popular as it provides the capabilities of exhaustively exploring the state space of the modeled system and generate counterexamples for properties specified over the model. The generated counterexamples can be used to derive test cases. However, counterexamples only show states, transitions and the values of their parameters. In addition, its semantics are also dependent on model specification languages and trace representation notations. In this paper, we present a focused test case generation approach from PAT model checker. The focus is driven by specific and putative attack behaviors. To this end, we devised test case specification rules to translate counterexamples to test cases. We demonstrate our approach by using air traffic control system (ATC) with a goal of minimizing safety risks due to cyberattacks during aircraft landing operation.