Model-based testing of NASA´s OSAL API — An experience report

We present a case study that evaluates the applicability and effectiveness of model-based testing in detecting bugs in real-world, mission-critical systems. NASA´s Operating System ion Layer (OSAL) is the subject system of this paper. The OSAL is a reusable framework that wraps several operating systems (OS) and is used extensively in NASA´s flight software missions. We developed a suite of behavioral models, represented as hierarchical finite state machines (FSMs), of the core file system API and generated a large number of test cases automatically. We then automatically executed these test cases against the OSAL. The results show that the OSAL is a high quality product. Naturally, due to the systematic and rigorous nature of MBT, we detected a few previously unknown “corner-case” bugs and issues, which escaped traditional manual testing and code reviews. We discuss the MBT architecture, the detected bugs, the code coverage of generated tests, as well as threats to validity of the study.