Embedded software, unlike general software, is highly dependent on the hardware they are developed for. Thus it became essential to create a hardware-based or hardware-like environment simultaneously with the software for effective testing. Where simulators and emulators can, up to some extent, provide a hardware-like environment for testing embedded software, they can not always be relied upon while testing for safety-critical applications like flight control system. It is this, high dependency on hardware, which makes testing, verification, and validation of embedded Softwares far more demanding than of general software. Moreover, several safety-critical embedded systems are also strictly real-time, or at least soft real-time, which requires timing properties to be verified in tandem with functional properties. In this blog post, we will look at a holistic view of various types of techniques like HIL(Hardware-in-the-loop) simulation, Timed automata, model checker, etc. which are used for testing, validation, and verification of soft/hard real-time embedded software.
Validation techniques for embedded software
Validation is mainly concerned with the question of whether the software that is being built is by the user’s demands and requirements. It answers the question, “Did we built the right product?”. In the case of real-time embedded systems, there are several types of validations like model validations, performance validation, communication validation, functionality validation, etc. that need to be carried out.
Model validation:
In model-based validation, we apply validation methods on high-level abstractions, i.e., on inter-component behavior of the system without looking deeply at the implementation of different components. There are several ways of specifying a model like data-flow graphs, finite state machines, timed automata, hybrid automata, concurrent/hierarchical state machines, message sequence charts, etc. Later on, these specifications are given to a model checker like SPIN, CBMC, SuSVM, etc. for validation.
Performance validation:
It focuses on the verification of the timing properties of a system—various techniques like Real-time calculus(RTC), WCET calculation, microarchitectural modeling, etc. External interferences like through interrupts, preemption, etc. are also taken into account while estimating timing properties.
Communication validation:
Communication validation is about validating the inter-component communication protocols, i.e., validating the interfaces responsible for connecting two different components of a system.
Functional validation:
It often refers to the validation of the low-level implementation of different components. It is different from model verification in a way that verifies implementation, whereas model validation verifies specifications. It is usually often carried out by dynamic traces, directed testing, etc.
Verification techniques for embedded software
Verification deals with the question, “Did we built the product, right?”. It focuses on efficiency, consistency, completeness, and correctness of the software that is being made. There are several techniques like static, dynamic, or hybrid for performing verification of the software or its components.
Dynamic techniques
Unlike static techniques, dynamic techniques like testing, co-simulation, assertion-based verification require simulators or actual target hardware and have an advantage that the entire software-hardware system is analyzed together.
- Testing: While testing, the complete hardware-software system is executed multiple times with different sets of input values under different environmental conditions(if they vary in a given system). Metric driven verification is, in fact, an amalgamation of testing techniques with coverage matrices. It can be further decomposed into unit testing, system testing, integration testing, etc.
- Assertion-based verification monitors a pre-specified condition during run-time. Several variants of assertion-based techniques are used for verifying SoCs along with the software.
Static techniques
Without actually running the code, static approaches tend to form the correctness of software by analyzing either the specification or the actual implementation(source code/compiled binary) or sometimes both. It mainly focuses on abstract static analysis, theorem proving, and model checking.
- Static analysis is used for various applications like WCET estimation, memory(stack/heap) usage estimation, invariant loop verification, array bound analysis, etc. It is based on abstract interpretation theory.
- Model-checking(MC) verifies the model of the software against the specification. It is mainly of two types: explicit model checking and symbolic model checking. Explicit state model checking(like SPIN) explicitly stores the explored state in a data structure like a hash table. In contrast, a symbolic model checker symbolically stores the explored states given by the state-transition function. Symbolic MC is broadly based on two concepts BDD(Binary decision diagrams) or SAT(Satisfiability theory). To prevent state space explosion while model checking of large software, we either use abstractions or a bounded MC or some times both.
- Theorem provers use a set of inference rules and axioms to prove the software against a given property. Despite the existence of automatic theorem provers(ATP), some manual interference is usually required to construct a proof.
Hybrid techniques
It combines both the static and dynamic approaches to overcome each other’s weaknesses. Predicate abstraction approaches and SMT(satisfiability modulo theory) are a few important examples of hybrid techniques that combine theorem proving with model checking. Predicate abstraction works on an abstract-check-refine paradigm where an abstract model is refined with every iteration. This is one of the most popular approaches for verification fo embedded software where simulations are used in tandem with model-checking based approaches.
Usually, during verification of embedded software, a top-down approach is used in which the software, during initial stages of development, is first tested using a model-in-loop(MIL) approach, which captures the intended behavior of the software model by recoding block state data and output. Then, the Software-in-loop approach(SIL) is used to compile and execute the code on a simulator. After that, the software is finally deployed for testing on actual hardware, which is known as hardware-in-loop(HIL) testing.
References:
- Lettnin, Djones, and Markus Winterholer. “An Overview About Debugging and Verification Techniques for Embedded Software.” Embedded Software Verification and Debugging. Springer, New York, NY, 2017. 1-18.
- Arons, Tamarah, et al. “Embedded software validation: Applying formal techniques for coverage and test generation.” Seventh International Workshop on Microprocessor Test and Verification (MTV’06). IEEE, 2006.
- Shah, Syed Muslim, and Muhammad Irfan. “Embedded hardware/software verification and validation using hardware-in-the-loop simulation.” Proceedings of the IEEE Symposium on Emerging Technologies, 2005… IEEE, 2005.
- http://www.cs.cmu.edu/~weigand/aro/presentations/cmu_clarke.pdf
- Guideline for Validation & VerificationReal-Time Embedded Software Systems
- Pierre, Laurence, and Martial Chabot. “Assertion-based verification for soc models and identification of key events.” 2017 Euromicro Conference on Digital System Design (DSD). IEEE, 2017.
- Roychoudhury, Abhik. Embedded systems and software validation. Morgan Kaufmann, 2009.