Many industrial systems that are developed without proper engineering guidance due to a lack of expertise or resources suffer from failures and maintenance problems in their evolving lifecycle. For mission-critical systems, in particular, ensuring high quality of non-functional requirements in a rapidly changing domain environment is of the utmost importance. In this paper, we report our case study with an industry system, a sensor-based earthquake warning system that was developed without a rigorous engineering process. Therefore, no requirements documents are available for future maintenance and verification. In this study, we used various types of software analysis methods such as stakeholder interviews, document reviews, source code analysis, model checking, and software testing for discovering requirements and also for verification purposes. We used a goal modeling approach to gather a set of initial requirements as though they had been elicited using an appropriate requirements engineering method in the early stage of the development process. Furthermore, software testing and model checking were iteratively used to verify and clarify unknown-source, uncertain, and unconfirmed requirements during the revision of the goal model. This study also provides an architectural improvement of the system through the discovery of requirements conflicts and violations. The experience and findings of this study, which demonstrate the effectiveness of applying diverse software engineering techniques in maintenance, can contribute to the analysis and evolution of systems developed without a proper engineering process, by discovering and verifying some critical requirements specifications.

Summary Embedded control software that controls safety‐critical IoT devices requires systematic and comprehensive verification to ensure safe operation of the device. However, rigorous verification in this domain has not been feasible due to the high complexity of embedded control software, which is characterized by the frequent use of multi‐tasking, interrupts, and periodic alarms. Realizing that two major factors, scalability and exactness, are extremely difficult to achieve at the same time but critical for effective and efficient verification in this domain, this work introduces a domain‐specific compositional OS‐in‐the‐Loop (OiL) verification approach and sets out to push the boundary in achieving both factors. The suggested approach (1) models the behavior of the underlying operating system to limit the search space using the notion of controlled concurrency, (2) performs heterogeneous composition of controllers with the formal OS model to reduce verification complexity, and (3) utilizes state‐of‐the‐art verification techniques for the purpose of comprehensive verification up to a given search depth.

Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive verification of multitasking embedded software together with its underlying operating system is very costly and impractical. To reduce the verification cost while achieving the desired accuracy, we propose a variant of CEGAR, named OiL-CEGAR (OS-in-the-Loop Counterexample-Guided Abstraction Refinement), where a composition of a formal OS model and an abstracted application program is used for comprehensive verification and is successively refined using the counterexamples generated from the composition model. The refinement process utilizes the scheduling information in the counterexample, which acts as a mini-OS to check the executability of the counterexample trace on the concrete program. Our experiments using a prototype implementation of OiL-CEGAR show that OiL-CEGAR greatly improves the accuracy and efficiency of property checking in this domain. It automatically removed all false alarms and accomplished property checking within an average of 476 seconds over a set of multitasking programs, whereas model checking using existing approaches over the same set of programs either showed an accuracy of under 11.1% or was unable to finish the verification due to timeout.

Automated unit testing reduces manual effort to write unit test drivers/stubs and generate unit test inputs. However, automatically generated unit test drivers/stubs raise false alarms because they often over-approximate real contexts of a target function f and allow infeasible executions of f. To solve this problem, we have developed a concolic unit testing technique CONBRIO. To provide realistic context to f, it constructs an extended unit of f that consists of f and closely relevant functions to f. Also, CONBRIO filters out a false alarm by checking feasibility of a corresponding symbolic execution path with regard to f's symbolic calling contexts obtained by combining symbolic execution paths of f's closely related predecessor functions.

This paper presents an approach to use C language to model underlying operating systems widely used in the domain of automotive control software. The greatest benefit of using C, a programming language, which is used widely in this domain, is the elimination of the heterogeneity between OS model and control software. This enables us to formally verify control software while keeping its own characteristics such as function calls, the use of external libraries, and dynamic memory allocation. We took a two-step approach to maintain the level of abstraction; we first define formal CSP models of OS components based on the OSEK/VDX international standard and then define an OS model in C by using the CSP models as references. We derived 20 functional API assertions, 6 invariant properties, 4 temporal properties and 4 code-safety properties from the OSEK/VDX international standard, and validated the model with the C code model checker CBMC. We used our OS C model to verify applications for Erika OS and could find out severe property violations.

Operating systems for embedded software publish a set of API functions together with a set of API-call constraints that have to be followed by application software running on the OS. If the embedded software is controlling safety-critical systems, a violation of those constraints may be a source of massive property damage or human injury. As a light-weight support for pre-checking such constraints during the development of embedded software, this work presents an API-call constraint checker for automotive control software. The checker converts application source code into formal models and checks violations of a set of pre-defined constraint patterns from OSEK/VDX international standard using model checker NuSMV. It is capable of checking local constraints within a task as well as global constraints involving task scheduling without suffering from false/missed alarms, by using formal models of the underlying operating system. We demonstrate the efficiency and effectiveness of the checker through comparative experiments with our previous checker which did not use the formal OS model.

This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reach ability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraint-based test generation using Maude can be as effective as that of using NuS MV, a state machine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

Model checking is an effective technique used to identify subtle problems in software safety using a comprehensive search algorithm. However, this comprehensiveness requires a large number of resources and is often too expensive to be applied in practice. This work strives to find a practical solution to model-checking automotive operating systems for the purpose of safety analysis, with minimum requirements and a systematic engineering approach for applying the technique in practice. The paper presents methods for converting the Trampoline kernel code into formal models for the model checker SPIN, a series of experiments using an incremental verification approach, and the use of embedded C constructs for performance improvement. The conversion methods include functional modularization and treatment for hardware-dependent code, such as memory access for context switching. The incremental verification approach aims at increasing the level of confidence in the verification even when comprehensiveness cannot be provided because of the limitations of the hardware resource. We also report on potential safety issues found in the Trampoline operating system during the experiments and present experimental evidence of the performance improvement using the embedded C constructs in SPIN. Copyright © 2012 John Wiley & Sons, Ltd.

Abstract In today’s information society, flash memory has become a virtually indispensable component, particularly for mobile devices. In order for mobile devices to operate successfully, it is essential that flash memory be controlled correctly through flash storage platform software such as the file system, flash translation layer, and low-level device drivers. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the software due to the difficulty of creating effective test cases. As a different approach, model checking techniques guarantee a complete analysis, but only on a limited scale. In this paper, we describe an empirical study wherein a concolic testing method is applied to the multi-sector read operation for flash storage platform software. This method combines a concrete dynamic execution and a symbolic execution to automatically generate test cases for full path coverage. Through the experiments, we analyze the advantages and weaknesses of the concolic testing approach on the flash storage platform software.

Model checking is an effective technique used to identify subtle problems in software safety. Its comprehensive search method on system state space provides high-level confidence regarding verification results, and its automated counterexample generation facility is a useful tool for tracing potential safety bugs. However, this comprehensiveness requires a large amount of resources and is often too expensive to be applied in practice. This work reports our experience with the software safety analysis of the Trampoline operating system using model checking. Trampoline OS is an open source operating system for automotive electronic/electrical devices based on the OSEK/VDX international standard. We present methods for converting the Trampoline kernel code into formal models and a series of experiments using an incremental verification approach. The conversion methods include functional modularization and treatment for hardware-dependent code, such as context-switching behavior. The incremental verification approach aims at increasing the level of confidence in the verification even when comprehensiveness cannot be provided due to the limitations of the hardware resource. We also report on a safety bug found in the Trampoline kernel during the experiments.

This paper proposes a systematic composition method for supporting both top-down and bottom-up approaches within the same frame. The method composes behavioral models of unit(abstract) components with respect to the services to be provided by the abstract component after the composition. Adapted from the standard operations in process algebra, two types of abstract techniques, synchronized abstraction and projection abstraction, are introduced to abstract the compositional behavior of components depending on their port connections and bindings. This method enables systematic extraction of high-level component behavior and reduces the complexity of composition and verification. Experiments show that performance improves when compositions are verified formally.

Flash memory has become virtually indispensable in most mobile devices, such as mobile phones, digital cameras, mp3 players, etc. In order for mobile devices to successfully provide services, it is essential that flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the complex device driver software. This deficiency incurs significant development and operation overhead to the manufacturers. As a complementary approach to improve the reliability of embedded software, model checking provides a complete analysis of a target model but the size of the target software is limited due to the state explosion problem.In this project, we have verified the correctness of a multi-sector read operation of Samsung OneNANDTM flash device driver by using both model checking and testing. We started the verification task with the model checkers NuSMV and Spin for an exhaustive analysis of a small size flash as a pre-testing step. We then set up a testbed based on a formal model used for model checking and performed testing on a large size flash. Through these verification tasks, we could successfully verify the correctness of the multi-sector read operation with both complete exploration of model checking and scalability of testing.

As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time; a feature suitable for regression verification.

Inaccuracies, or deviations, in the measurements of monitored variables in a control system are facts of life that control software must accommodate $the software is expected to continue functioning correctly in the face of an expected range of deviations in the inputs. Deviation analysis can be used to determine how a software specification will behave in the face of such deviations in data from the environment. The idea is to describe the correct values of an environmental quantity; along with a range of potential deviations, and then determine the effects on the outputs of the system. The analyst can then check whether the behavior of the software is acceptable with respect to these deviations. In this report we wish to propose a new approach to deviation analysis using model checking techniques. This approach allows for more precise analysis than previous techniques, and refocuses deviation analysis from an exploratory analysis to a verification task, allowing us to investigate a different range of questions regarding a system's response to deviations.

Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction techniques have been proposed to address this problem. In this paper, we wish to propose domain abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system. Our technique is automatable with some minor restrictions.