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 pairwise 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.
Keywords - embedded system, verification, model checking, generation of verification items, case study
※This report which the authers contributed to APSEC2013 is placed in this magazine under the license of the IEEE.