다중 조건 커버리지 기반의 논리식 동등성 검사기 개발

Development of a Logic Expression Equivalence Checker Based on Multiple Condition Coverage

MC/DC(Modified Condition/Decision Coverage)는 각 조건이 결정문 결과에 미치는 독립적 영향을 입증하도록 요구함으로써, MCC(Multiple Condition Coverage)대비 적은 테스트 케이스로 코드의 논리적 오류를 검출하는데 효율적인 코드 커버리지 기준이다. 안전 필수 시스템 검증에 널리 사용되는 MC/DC는 테스트 케이스 생성을 위한 다양한 연구가 진행되어 왔으나, 이들은 공통적으로 논리식 전처리 과정의 신뢰성이 보장된다는 가정하에 알고리즘의 효율성 향상에만 초점을 맞추어 왔다. 논리식의 전처리 과정의 동등성을 검증하지 않으면 원본 논리식과 다른 논리식을 테스트할 수 있는 잠재적인 위험을 내포하고 있다. 이러한 논리식 전처리 과정의 신뢰성 검증 문제를 해결하고자, 본 연구는 MCC 기반의 논리식 동등성 검사기를 개발한다. 개발한 논리적 동등성 검사기는 논리식의 각 변환 단계가 이전 단계와의 동등성을 유지하는지 순차적으로 검증하며, 불일치가 발견된 최초의 단계와 해당 반례를 제공하여 오류의 원인을 신속하게 파악하도록 돕는다. 이는 MCC를 만족하는 모든 입력 조합, 즉 전체 진리표를 생성하여 두 논리식의 결과를 비교하는 방식으로 이루어진다. 본 연구는 논리식 전처리 단계의 신뢰성 문제를 해결함으로써, MC/DC 연구 프로세스의 결과 신뢰도를 전반적으로 개선하는 데 기여할 것이다.

Modified Condition/Decision Coverage(MC/DC) is a widely adopted criterion in safety-critical systems, offering a more efficient alternative to Multiple Condition Coverage(MCC). However, existing research on MC/DC test generation has primarily prioritized algorithmic efficiency, often overlooking the reliability of the prerequisite boolean preprocessing step. This implicit assumption of reliability poses a significant risk, as errors during preprocessing can result in the testing of logically non-equivalent expressions. To ensure the integrity of the preprocessing phase, this paper proposes an MCC-based logical equivalence checker. This tool verifies equivalence sequentially at each step by comparing outcomes across all MCC combinations, thereby covering the complete truth table. If a discrepancy is detected, the tool identifies the initial failing stage and provides a corresponding counterexample. By guaranteeing the correctness of the logical expression preprocessing, this research contributes to enhancing the overall reliability of MC/DC testing.