A Case Study: Verification of Specifications of an Embedded System and Generation of Verification Items Using Pairwise Testing

Ensuring the reliability of embedded systems has become very important. Reliability may be ensured by a number of formal methods. We study one such verification technique by applying it to an in-house development product in Mitsubishi Space Software Co., Ltd. This is a practical industrial case study, we describe our approaches and present verification results. Our aim is to check the correctness of specifications which include a set of constraints on parameters individually called an evaluation item. To that end, we adopt model checking and satisfiability checking. In our study, we set conversion rules from specifications to formal models. Part of the conversion is done by hand in this study. Manual generation limits the preparation of individual evaluation items. To overcome this limitation we present an approach for automatically generating combinations of parameters for verification by applying the pair wise testing method. Finally, we present experimental results. Note that the application of formal techniques, in this setting, is still in its preliminary stages. It is intended to develop formal techniques to the point where products may be automatically verified.