Qplus-AIR is a real-time operating system for avionics, and its safety and correctness should be analyzed and guaranteed. We performed model checking a version of Qplus-AIR with the Times model checker and identified one abnormal case that might result in safety-critical situations.

Two structural coverage criteria, toggle coverage and modified condition/decision coverage, for FBD (Function Block Diagram) simulation are proposed in the previous study. This paper empirically evaluates how effective the coverage criteria are to detect faults in an FBD program using the mutation analysis.