MCAPI Predictive Verification Tool (MPVT)

We develop dynamic predictive verification techniques that allow us to find actual and potential errors in a multicore software. We have two types of verification, assertion verification and deadlock/race condition detection. An assertion is a property expressed using variables on processes. e.g., more than one process is in critical section. Assertion Verification is determining if an execution trace satisfies the assertion. Given a multicore program and a property, our automated verification flow consists of the following steps, where we can turn on and off each type of verification or use them in conjunction.
  1. The property is read, and the variables are found.
  2. Tracing functions for relevant variables and shared variables are automatically added to the program.
  3. The instrumented program is compiled and executed with our MCAPI Verification Library, generating a partial order trace.
  4. The deadlocks and race conditions are detected during execution of the instrumented program.
  5. The resulting partial order trace and the property are passed to the BTV verifier tool, which determines whether the property is satisfied or not.

 

MCAPI Mutation Testing Tool (MMTT)

Mutation testing is a software testing method that involves inserting faults into user programs and then re-running a test set against the mutated program. A good test will detect the change in the program. Mutation testing allows us to have a verification coverage measure which we perform with the following steps:
  1. We create a set of mutant programs. In other words, each mutant program differs from the original program by one mutation. For example, one single syntax change made to one of the program statements.
  2. We run the original program and the mutant program with the same test set.
  3. We evaluate the results, based on the following set of criteria: If both the original program and the mutant program generate the same output, our test set is inadequate. Our test set is adequate, if one of the tests in the test set detects the fault in our program. That is, one mutant program generates a different output than the original program.
Each change of the program by a mutation operator generates a mutant multicore program. A mutant is killed (detected) by a test case that causes it to produce different output from the original multicore program. The ratio of the number of mutants killed to the number of all mutants is called mutation coverage. MTT is a tool that automatically generates mutation coverage for MCAPI user applications.

 

Publications

  • Etem Deniz, Alper Sen, and Jim Holt, "Verification Coverage of Embedded Multicore Applications", Design, Automation and Test in Europe Conference (DATE), 2012. PDF
  • Etem Deniz, Alper Sen, and Jim Holt, "Verification and Coverage of Message Passing Multicore Applications", ACM Transactions on Design Automation of Electronic Systems (TODAES), 2012. PDF

    •  

    Source Code

    The source code can be downloaded here.

     

    Contact

    If you have any comment, questions, suggestions, or want to contribute to MPVT or MMTT, please feel free to contact us at: etem.deniz at boun dot edu dot tr