Using a Virtual Machine Environment for Formal Verification Credit

Test Embedded Avionics Software in a Virtual Machine Environment

There are several quality benefits of using a virtual machine environment to test embedded avionics software. A virtual machine environment is intended for testing both high-level and low-level software requirements. In this blog, we will look at a strategy for performing formal software testing in that environment and specifically address hardware/software integration testing issues.

A virtual machine consists of an emulation of a processor and I/O components in order to run the unaltered target code binaries in an environment that closely resembles the target hardware. The goal is to provide a development and test environment that is transparent to the flight software and for the end user to have more access, more control,
and better debugging capabilities than they would on real target hardware. Virtual machines also help to solve problems with hardware availability that cause bottlenecks for development and test efforts.

JETS Virtualization

JETS is Performance’s virtualization solution. It was initially created in 2008 to support a large requirement-based test development effort on the Boeing 787. From 2008 to 2014, JETS was used as an internal tool to help Performance be successful on programs that had HW limitations. Performance’s use of JETS has allowed us to realize the benefits of Virtualization on several programs. JETS allowed Performance to maintain quality in both development and test activities when hardware availability and or debug capability were limited. Performance is now offering JETS as a product to gain these benefits on more programs.

Virtual Machines

A virtual machine uses an instruction set emulator; the same instructions on the real hardware perform the same operations in the emulation. Hardware timers are implemented to have the same resolution as real hardware, however they can be sped up or slowed down to help with debugging.

Hardware peripherals are implemented to act like the real hardware from the software’s point of view. The I/O is then simulated and customized for the environment. The I/O can be captured and/or injected to aid in debugging or as part of testing. In this simulated state, the I/O can easily communicate with other virtualized machines running on the same machine or other networked machines allowing simulations of larger systems. The I/O can also be connected to real I/O as required to communicate with other real hardware devices. For instance, ARINC 429, ARINC 664, analog, and discrete cards connected to the host machine can connect the simulated I/O with real world I/O. This allows the possibility of running one or more virtual machines that fully interact with any number of real hardware machines. Integration with any mix of virtualization and hardware is possible as long as the appropriate communication interfaces are provided.

Benefits of Using VMs

There are many benefits to using virtualization for program development and verification including increased debugging capability, test environment reproducibility, greater I/O, and hardware control. Through more control, easier automation of testing, and easier regression testing, virtualization can drive higher quality into the software. Increased quality drives additional benefits such as reduced open problem reports, improved verification efficiency, reduced schedule, and increased safety.

Development and Debugging

A virtual machine can provide debug capability above and beyond what is available on hardware. Software development can start before actual hardware becomes available. There is also reduced dependency on hardware even when hardware is available. Once set up, the development environment is easily replicated for each developer on their local PC which reduces the need for target hardware.

Debugging, especially with low-level code, is often a difficult task that takes significant time on the real hardware. With virtualization, debugging can be performed using a standard debugger such as GDB. The debugger can start where the Program Counter starts execution which allows debugging of low-level boot strap code and Board Support Packages (BSPs). Using virtual machines opens up other tool possibilities to aid in development such as logging within the emulation to help debug register access and bus traffic. Other possible tools can be created for hardware device manipulation, memory address viewing without halting, invalid memory access reporting, single/double event upsets, and stack monitoring. This functionality is possible since the emulator is in control of all executed instructions and can be set up to report various activities.

Configuration Control and Distribution

A virtual machine provides advantages for configuration and distribution. It is possible to keep the virtual machine in step with the real hardware development as each new board revision is released. Since the machine is software, each revision can easily be stored in a Configuration Management system for portability and predictable reproducibility. In an environment with increasingly distributed teams this can ensure everyone is working from the same baseline.

Software Verification

Software verification in a virtual machine has advantages in automation, regression testing, and error injection capability. Creating an automated test environment is much easier when running with simulated I/O compared with a real hardware setup in a lab.

A suite of automated test scripts makes regression testing much easier to run and does not require precious lab time. A machine or set of machines can be set up to run regression testing for every build, intermediate build, or as often as desired. This regression testing can help to find software problems earlier in the development life cycle. Later in the life cycle, this method easily allows a larger set of regression tests to be run without spending as much time analyzing which subset of tests should be run for a software change. This can cut down on the likelihood of missing errors introduced by software changes.

Performing verification in a virtual machine allows more testing of error/failure related requirements. Oftentimes these requirements cannot be adequately tested with real target hardware or it is very time consuming and expensive to do so. An advantage of using simulated peripherals is the ability to inject errors. With error injection capabilities, the software requirements addressing error detection and response can be tested in an easier and automated manner. This can replace analysis/inspection tests and allow additional robustness testing that was previously not obtainable.

Structural Coverage

Structural coverage can be performed in the virtual machine and provides additional tools/solutions when dealing with some of the problems often encountered. In a virtual machine, the memory size can be increased, to the maximum addressable size, to allow for full object code instrumentation in systems with limited memory on the real hardware. When dealing with older, slower processors, the virtualized version could execute faster than the real hardware to overcome performance constraints that were preventing or limiting instrumentation. This environment also has the possibility to gather structural coverage at the machine code level and without instrumentation. (Note: This capability would need qualification.)

Systems Validation/Verification

A potential use of virtualization is for early systems validation. Since hardware and software can be prototyped, systems validation to confirm requirements are correct and complete can occur prior to hardware production. This validation can occur for a single hardware device or multiple devices in a more complex system. Early validation should lead to less change later in the development process.

An environment can be created to allow the same systems tests to be run in the virtual machine(s) as well as a real systems lab. That would allow a virtualized system to aid in development and debug of systems level testing. The environment could also be used to aid in reproducing and debugging system level issues.

Plan for Certification Credit

When used for formal testing, the qualification of the virtual machine must be considered based on the types of formal testing to be performed. Per DO-330 Appendix D, section 1.3: an emulator or simulator tool qualification is required if it is used for hardware/software integration testing. Therefore, we address guidelines for the case where hardware/software integration testing is planned to be run for formal credit in the virtual machine and when it is not.

Qualifying the Virtual Machine

In the case where hardware/software integration testing is to be run for formal credit in the virtual machine, the virtual machine will need to be qualified as a test tool. Since this type of tool could fail to detect an error with the hardware/software integration, DO-178C section 12.2.2 indicates TQL-5 for all design assurance levels of software. It is highly likely that not all of the hardware is emulated to the level where all aspects are equivalent to the real hardware. In this case, only the software requirements related to the fully emulated and qualified hardware features can be formally tested in this environment.


Below are examples of HW interfaces for qualification from DO-178C section 6.4.3.a:

  • Interrupt handling
  • BIT to failure detection
  • HW/SW interfaces
  • Control of memory management hardware or other hardware devices under SW control
  • Stack overflow
  • SW partitioning
  • Responses to hardware failures
  • Behavior of control loops
  • Single event upset detection
  • Software timing that is the result of timer-driven interrupts or hardware-driven timer activities
  • Bus/resource contention issues
  • Responses to hardware transients

Depending on how the virtual machine is created, timing errors may not be detectable and therefore not qualifiable for execution time requirements. For example, if the software timing is based on a hardware timer interrupt and that hardware timer interrupt is properly simulated and qualified, then the software timing requirements based on those timers should be formally verifiable in that environment. If the software contains low-level instruction-based timing such as using a no-op loop, then the simulation would need to implement instruction level timing to qualify the environment to test that level of timing. Without properly emulating instruction level timing, the environment would also not be suitable for worst-case timing analysis.

The following example scenario illustrates the type of timing test that can be run formally in the qualified simulated environment:

  • The software application is running at 10 Hz.
  • The application timing is controlled by a timer interrupt.
  • A requirement states to perform a task once per second.
  • The code uses either a hardware timer or frame counting method to track time.
  • The timer interrupt portion of the environment is qualified.

The Tool Operational Requirements (TOR) should cover equivalency and error detection capabilities. For the equivalency TOR, qualifying a virtual machine should focus on equivalence to target hardware. The TOR need to cover the operational aspects of the hardware that affect the HW/SW integration tests intended to be run in the environment. The TOR based tests need to be run on both environments to provide evidence of their equivalence.

The error detection TOR identify the functionality to detect errors. The TOR based tests for these requirements would be run on the virtual machine to demonstrate errors are correctly detected.

Sample Requirements for Equivalency:

The tool shall emulate 64kbytes of RAM memory from address 0x00010000 to 0x0001FFFF.

The tool shall emulate the Power PC 604 instruction set.

Sample Requirements for Error Detection:

The tool shall log memory accesses outside the valid memory ranges.

Unqualified Virtual Machine

In the case where hardware/software integration testing will not be run for formal credit in the virtual machine, testing classified as software integration testing and low-level testing can be performed for formal credit without qualification of the environment. In this case, the executable object code tested is unchanged from target object code so the objectives to ensure the executable object code meets the requirements can be satisfied. Also, the objective for target computer compatibility is not considered to be eliminated, reduced, or automated since the hardware/software integration tests will be performed on the target hardware. If the test environment is set up to allow the same test scripts to be executed in both the virtualized and target hardware environments, then the hardware/software tests can be developed in the virtual machine but need to be run for formal credit in the target hardware environment.

Tests in this environment can also provide an improvement over “test by inspection.” Requirements for hardware failures that are difficult or impossible to inject on the target hardware could be tested on the virtual machine. Traditionally, these test cases have been performed by time-consuming analyses and could be replaced or augmented with automated tests in a virtual machine. An example of requirements that often fall into this category are Built in Test (BIT) for failure detection and responses to hardware failures.

In either situation, in order to properly track which requirements can be tested in the virtual machine, the requirements should be tagged as such and test case/procedure review should include a step to ensure the test was written for the correct environment. Furthermore, if the test environment is such that the same scripts can be run in the virtual machine and the target hardware environment, a check should be performed to ensure the formal results were obtained in the correct environment.

Note that even without qualification, some amount of hardware/software integration related testing could be augmented in the virtual machine. For instance, tests for hardware failures that are difficult or impossible to inject on the target hardware. Traditionally, these test cases have been performed by analysis. These time-consuming and error-prone analyses could be replaced or augmented with automated tests in a virtual machine. Examples include verifying Built in Test (BIT) for failure detection and responses to hardware failures.

DO-254 Implications

The use of a virtual machine for software testing does have some implications for DO-254 hardware testing. COTS CPUs are typically covered by SW tests executed on target (AC-20-152). To satisfy this requirement, a subset of the test still needs to be run on the target hardware if a virtual machine is used for the software testing. If the virtual machine is to be qualified then the tool qualification tests that are run for equivalence on the real hardware can be used to satisfy the DO-254 requirement. If the virtual machine is not going to be qualified, then the software tests that satisfy hardware/software integration that are going to be run on the target hardware can be used to satisfy the DO-254 requirement. If neither of these conditions apply, then some other means, such as running a subset of the software tests on the target hardware, will need to be used in order to satisfy the DO-254 requirement.

The use of virtual machines for formal test efforts can improve efficiency and quality through earlier systems validation, reduction of HW dependencies, earlier and improved debugging capabilities, easier configuration control and distribution, more complete regression testing, and more thorough testing through reduction of “test by inspection.” Qualification of virtual machine test environment may provide even more benefits over a non-qualified version.

Performance Software

Performance was founded in 1998 and mainly provides DO-178 Software and Systems Engineering Products and Services. Performance has around 220 employees located at six sites across the United States with headquarters in Phoenix, Arizona. Performance is recognized as a Preferred Supplier/Vendor to many of our key customers.

Performance’s competencies/experience includes:

  • DO-178B/C using Customer Specific Processes
    • Completed more than 200 DO-178B/C Level A-D programs.
  • DO-178B/C using Performance Process
    • Design Assurance Levels A through D.
  • DO-200A FAA LOA:
    • Airport Map Database
  • ARP-4754A
    • System requirements, verification, and validation on several programs.
  • DO-254
    • Several verification programs for DAL A-C.

Performance’s products include Airport Map Databases (AMDB), Off Aircraft Dataloader, embedded Dataload libraries, and JETS Virtualization.

Jets Virtual Platformvirtualization