Title :
A Case Study: Verification of Specifications of an Embedded System and Generation of Verification Items Using Pairwise Testing
Author :
Sekizawa, Toshifusa ; Kotorii, Tsugu
Author_Institution :
Fac. of Inf., Osaka Gakuin Univ., Suita, Japan
Abstract :
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.
Keywords :
computability; embedded systems; formal specification; formal verification; program testing; software reliability; embedded systems reliability; formal methods; in-house development product; model checking; pairwise testing method; satisfiability checking; specification correctness checking; specification verification; verification item generation; Embedded systems; Model checking; Product development; Radiation detectors; Reliability; case study; embedded system; generation of verification items; model checking; verification;
Conference_Titel :
Software Engineering Conference (APSEC), 2013 20th Asia-Pacific
Conference_Location :
Bangkok
Print_ISBN :
978-1-4799-2143-0
DOI :
10.1109/APSEC.2013.130