title: Formal verification of an application framework of Benchmark Electronics Almelo
company: Benchmark Electronics Almelo
keywords: Verification, Application Framework
topics: Case studies and Applications , Logics and semantics
committee: Marieke Huisman ,
Oskar Klooster

Description

Benchmark Electronics (https://www.bench.com/) is a global provider of design engineering services for original equipment manufacturers (OEM). One of our design sites is in Almelo (https://www.bench.com/company/worldwide-locations/europe/almelo-netherlands), where we offer both manufacturing and design engineering. In Almelo, we are developing an application framework that contains functionality that most of our customers need. This C++ framework currently consists of:

  • Data objects that automatically report changes to registered observers
  • Command objects that automatically report on the progress
  • Controller objects that support a phased initialization of an application
  • Abstract serial communication object for inter-processor communication
  • Inter-processor protocol for
    • starting and stopping command objects
    • communicating command progress
    • communicating data object changes

With our customers ranging from industrial to medical and avionics OEMS, our software must be extremely stable and robust. Most software is being developed according to the latest IEC 62304 standard for medical device software, which is required to comply with both the EU and USA law. In addition, rigorous continuous integration and testing have resulted in a high-quality standard of the software we create.

Nevertheless, we want to improve. In our highly competitive market, we cannot afford to be content and relax. We need to become more efficient at writing high-quality software, which is why we are always exploring new tools. The VerCors toolset seems promising to us, as it can detect concurrency issues and other programming errors, when used correctly. However, in its current state, the VerCors toolset cannot be applied to our application framework; the C++ language is not yet supported and its user friendliness needs to be improved.

This MSC project investigates if it is feasible to use the VerCors toolset for formal verification of the application framework of Benchmark Almelo. The goals of this project would be to:

  • List the types of verification from which the application framework would benefit most, e.g.
    • Detect dead-locks in initialization and communication
    • Detect race conditions in handling data objects and command states
    • Detect out-of-bounds access of arrays and lists
    • Etc.
  • Annotate (part of) the framework for these types of verification
  • Add C++ (or a workable subset) as an input language to the VerCors toolset
  • Verify the annotated part of the framework with the VerCors toolset
  • Make recommendations for further support of this use case for the VerCors toolset

The project will be supervised jointly by Marieke Huisman (FMT) and Oskar Klooster (Benchmark Electronics).

REFERENCES

  1. The VerCors Tool for Verification of Concurrent Programs