Unlike random algorithms or Abstract Interpretation, Model Checking allows to analyze the dynamic behavior of software with mathematical completeness. Use cases are for example robustness analysis, structural test case generation or test case generation from requirements. However, the complexity of the analysis task makes it challenging to apply Model Checking to industrial applications.
The recent and much-noticed case study “Benchmarking Software Model Checkers on Automotive Code” at the 2020 NASA Formal Methods Symposium, co-authored by the distinguished expert for model checking Prof. Joost-Pieter Katoen, uncovers a “serious gap between the needs of automotive code verification and open-source software model checker capabilities”.
On 179 requirements for two large, floating-point dominated, industrial models from Ford Motor Company, the open-source academic model checkers were only able to cover at most 20% of these requirements, while various competitors only obtained results for 0% to 5%. Including bounded verification results, the commercial verification tool BTC EmbeddedPlatform however succeeded on 97% of the requirements.1
Precisely because all the academic software-verification tools perform very well in the annual prestigious “Competition on Software Verification” (SV-COMP), the question arises: Why is there such a tremendous discrepancy between academic model checkers and the commercial verification tool BTC EmbeddedPlatform on real-world industrial embedded software?
My answer to this is the power of focus! There are mainly three directions we laid the focus on to solve the problems of our customers by the underlying model checking technology within BTC EmbeddedPlatform.
1. Focus on effectiveness to solve the problem of your customer!
Since day one we address exactly the problem classes our customer needs to solve, i.e. large-sized auto-generated embedded code –on the one hand– with integer, floating point and pointer arithmetic, large look-up tables, and state-flow logic but –on the other hand– even without recursive functions, memory allocation, and full support of C libraries (as the latter is not present in safety-relevant embedded software).
In order to fulfill this high demand sustainably in the future, we have implemented a successful customer support managed by the Support department: new customer requests for unsupported code features are directly analyzed by the Innovation & Technology (I&T) department within a narrow time frame to give the customer immediate feedback. Based on this analysis and in close collaboration with Product Management and Product Development, a productive solution for the customer request is scheduled for an upcoming release of BTC EmbeddedPlatform.
Though needless to say, I would like to point out that each new code feature, namely in many diverse variants, finds its way into our powerful, huge, and still growing I&T Model Checking Test Suite. This test suite currently consists of a plethora of customer models and dedicated code fragments and is designed to assure our high-quality standards on correctness of our model checking technology in all its applications like formal verification, formal test, test case generation, and consistency, completeness & correctness analysis.
2. Focus on efficiency to solve the problem of your customer!
Of course, an effective solution for your customer’s problem is the first crucial step – but the solution must be applicable in practice as well and not only in theory! Concerning this matter, I remember a nice anecdote my dear colleague Dr. Tom Bienmüller (SVP Products) told me in those days I joined BTC Embedded Systems:
Model checking support for floating-point software was on our roadmap due to increasing use of IEEE-754-based floating-point processors in the field. Thanks to a large European research project we got in touch with Prof. Daniel Kroening from Oxford University, a distinguished expert for model checking, who developed the powerful state-of-the-art model checker CBMC together with the grand Prof. Edmund Clarke, one of the inventors of model checking. After having prototypically integrated CBMC into BTC EmbeddedPlatform – thus having established an effective approach to floating-point code analysis – Tom started a verification task right before end of the work day. When he came back to his office next morning there were bad and good news: Unfortunately, CBMC was still running without any progress — but his office was beautifully warm (Kindly note that it was wintertime).
It is worth mentioning that CBMC was the overall winner of the SV-COMP 2014. So why has CBMC failed here? I had the challenge to analyze this and even the honor to visit Daniel and work closely together with his wonderful team at Oxford University. To come straight to the point: After detailed analysis, it turned out that CBMC itself was not the problem but CBMC was simply not optimized for our use case. After some engineering effort in the integration and pre-processing tool chain and without changing any bit of CBMC, there were only good news remaining: “Tom’s verification task” could now be solved within fractions of a second — and his office was not heated up (In the meantime it was summer).
What I’m trying to say is when focusing on the actual problem it is often not necessary to do rocket science at the algorithmic core of model checkers but it might be sufficient to massage the input in such a way to fit the model checker’s needs.
3. Focus on diversity to solve the problem of your customer!
My personal mission, the mission of I&T as well as of our whole company is to maintain our leading role as a tool provider for next-generation verification and testing solutions for the development of embedded systems and software. To fulfill this mission, we steadily keep track of the state of the art in model checking research. Moreover, we are convinced that there is not only one solution to solve all problems but –quite the contrary– different problem classes require different problem-solving approaches!
Let me tell you another anecdote. When I was a young academic researcher, a long-established colleague of mine was hard working on a parallel problem solver to be well prepared for an international competition. He was optimizing his solver day and night on the deepest bit level (to utilize the CPU’s cache memory). When the day of competition came, he was very much disappointed. Another solver won the competition. But the worst was yet to come: The winning tool implemented a rather simple portfolio approach, i.e. let run multiple solvers in parallel until the first of them succeeds.
We pursue the very same latter strategy in BTC EmbeddedPlatform. One good example here is automatic test case generation in order to achieve high structural code coverage. The default heuristics first executes a simple but fast random test case generation and only after this the more sophisticated model checking technology is applied. This works like the Pareto principle: the random search usually achieves more than 80% code coverage in less than 20% of the runtime.
Another example: Due to its internal functionality based on so called bit-blasting, CBMC performs very well on embedded code containing bitwise operations and control logic but rapidly approaches its limits when it comes to more complex integer and floating-point arithmetic expressions. The latter has become more and more apparent in our customer’s software. Given the fact that most problem solvers are essentially based on the same bit-blasting technique, how could we address this new situation? Here again our strong academic network was of great value. During my time as PhD student at Oldenburg University, we have developed a novel model checking algorithm together with colleagues from Freiburg University. This new model checker called iSAT3 rests upon a diverse technique, namely interval arithmetic, and can efficiently cope with complex arithmetic expressions. In a transfer project with the involvement of both universities, we tailored iSAT3 to our use cases and successfully “transferred” it from academia to industry.
In addition to random search, CBMC, and iSAT3, we have three more model checkers running in BTC EmbeddedPlatform and we are currently investigating some more promising candidates – to be optimally prepared for new customer requests.
Conclusion
Coming back to the starting point of this article, i.e. the “serious gap between the needs of automotive code verification and open-source software model checker capabilities”, I have tried to explain why the commercial and customer-centric verification tool BTC EmbeddedPlatform performs so well in a real-world industrial setting. The authors of the case study recommend that “the software model checking community and industrial partners […] should […] set up a substantial set of industrial benchmarks” such that academia can also focus on real-world industrial problems. I absolutely appreciate such joint effort as this will lead to a gain for both sides: Academia can adjust their tools to industrial needs and thus increases the value of their research and industry can more smoothly utilize the academic tools in their projects and thus increases their product quality in a shortened design phase. There actually is a great power in focus as the Russian proverb suggests:
“If you chase two rabbits, you will not catch either one.”
With this in mind: Stay focused!
If you want to know more have a look at the Interview of Karsten Scheibler about how a model checker works.
