{"id":1675,"date":"2020-07-31T10:39:08","date_gmt":"2020-07-31T08:39:08","guid":{"rendered":"https:\/\/zen-cori.138-201-132-86.plesk.page\/?p=1675"},"modified":"2022-09-28T16:26:36","modified_gmt":"2022-09-28T07:26:36","slug":"the-power-of-focus-how-to-optimize-a-model-checker-for-embedded-software","status":"publish","type":"post","link":"https:\/\/www.btc-embedded.jp\/ja\/the-power-of-focus-how-to-optimize-a-model-checker-for-embedded-software\/","title":{"rendered":"The Power of Focus &#8211; How to Optimize a Model Checker for Embedded Software"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-post\" data-elementor-id=\"1675\" class=\"elementor elementor-1675\" data-elementor-post-type=\"post\">\n\t\t\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-3b5f0493 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"3b5f0493\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-559a247a\" data-id=\"559a247a\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t<div class=\"elementor-element elementor-element-da6f93a elementor-widget elementor-widget-heading\" data-id=\"da6f93a\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.20.0 - 26-03-2024 *\/\n.elementor-heading-title{padding:0;margin:0;line-height:1}.elementor-widget-heading .elementor-heading-title[class*=elementor-size-]>a{color:inherit;font-size:inherit;line-height:inherit}.elementor-widget-heading .elementor-heading-title.elementor-size-small{font-size:15px}.elementor-widget-heading .elementor-heading-title.elementor-size-medium{font-size:19px}.elementor-widget-heading .elementor-heading-title.elementor-size-large{font-size:29px}.elementor-widget-heading .elementor-heading-title.elementor-size-xl{font-size:39px}.elementor-widget-heading .elementor-heading-title.elementor-size-xxl{font-size:59px}<\/style><h2 class=\"elementor-heading-title elementor-size-default\">1. Focus on effectiveness to solve the problem of your customer!<\/h2>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-fa217fc elementor-widget elementor-widget-text-editor\" data-id=\"fa217fc\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.20.0 - 26-03-2024 *\/\n.elementor-widget-text-editor.elementor-drop-cap-view-stacked .elementor-drop-cap{background-color:#69727d;color:#fff}.elementor-widget-text-editor.elementor-drop-cap-view-framed .elementor-drop-cap{color:#69727d;border:3px solid;background-color:transparent}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap{margin-top:8px}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap-letter{width:1em;height:1em}.elementor-widget-text-editor .elementor-drop-cap{float:left;text-align:center;line-height:1;font-size:50px}.elementor-widget-text-editor .elementor-drop-cap-letter{display:inline-block}<\/style>\t\t\t\t<p>Since day one we address exactly the problem classes our customer needs to solve, i.e. large-sized auto-generated embedded code \u2013on the one hand\u2013\u00a0<b>with<\/b>\u00a0integer, floating point and pointer arithmetic, large look-up tables, and state-flow logic but \u2013on the other hand\u2013 even\u00a0<b>without<\/b>\u00a0recursive functions, memory allocation, and full support of C libraries (as the latter is not present in safety-relevant embedded software).<\/p><p>In order to fulfill this high demand sustainably in the future, we have implemented a successful customer support managed by the\u00a0<i>Support<\/i>\u00a0department: new customer requests for unsupported code features are directly analyzed by the\u00a0<i>Innovation &amp; Technology<\/i>\u00a0(I&amp;T) department within a narrow time frame to give the customer immediate feedback. Based on this analysis and in close collaboration with\u00a0<i>Product Management<\/i>\u00a0and\u00a0<i>Product Development<\/i>, a productive solution for the customer request is scheduled for an upcoming release of BTC Embedded<i>Platform<\/i>.<\/p><p>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\u00a0<i>I&amp;T Model Checking Test Suite<\/i>. 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 &amp; correctness analysis.<\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-d88eb76 elementor-widget elementor-widget-heading\" data-id=\"d88eb76\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">2. Focus on efficiency to solve the problem of your customer!<\/h2>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-e9bd924 elementor-widget elementor-widget-text-editor\" data-id=\"e9bd924\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<ol><li><p>Of course, an effective solution for your customer\u2019s problem is the first crucial step \u2013 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\u00fcller (SVP Products) told me in those days I joined BTC Embedded Systems:<\/p><p>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\u00a0<a href=\"https:\/\/en.wikipedia.org\/wiki\/Daniel_Kroening\" target=\"_blank\" rel=\"noopener\">Prof. Daniel Kroening<\/a>\u00a0from Oxford University, a distinguished expert for model checking, who developed the powerful state-of-the-art model checker\u00a0<a href=\"https:\/\/www.cprover.org\/cbmc\/\" target=\"_blank\" rel=\"noopener\">CBMC<\/a>\u00a0together with the grand\u00a0<a href=\"https:\/\/en.wikipedia.org\/wiki\/Edmund_M._Clarke\" target=\"_blank\" rel=\"noopener\">Prof. Edmund Clarke<\/a>, one of the inventors of model checking. After having prototypically integrated CBMC into BTC Embedded<i>Platform<\/i>\u00a0\u2013 thus having established an effective approach to floating-point code analysis \u2013 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 \u2014 but his office was beautifully warm (Kindly note that it was wintertime).<\/p><p>It is worth mentioning that CBMC was the overall winner of the\u00a0<a href=\"https:\/\/sv-comp.sosy-lab.org\/2014\/results\/index.php\" target=\"_blank\" rel=\"noopener\">SV-COMP 2014<\/a>. 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\u00a0<i>without<\/i>\u00a0changing any bit of CBMC, there were only good news remaining: \u201cTom\u2019s verification task\u201d could now be solved within fractions of a second \u2014 and his office was not heated up (In the meantime it was summer).<\/p><p>What I&#8217;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\u2019s needs.<\/p><\/li><\/ol><figure class=\"content-image \"><\/figure>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-3810d50 elementor-widget elementor-widget-heading\" data-id=\"3810d50\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">3. Focus on diversity to solve the problem of your customer!\n<\/h2>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6bb1d04 elementor-widget elementor-widget-text-editor\" data-id=\"6bb1d04\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p>My personal mission, the mission of I&amp;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\u00a0<b>not<\/b>\u00a0only one solution to solve all problems but \u2013quite the contrary\u2013 different problem classes require different problem-solving approaches!<\/p><p>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\u2019s 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.<\/p><p>We pursue the very same latter strategy in BTC Embedded<i>Platform<\/i>. 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\u00a0<i>random<\/i>\u00a0test 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.<\/p><p>Another example: Due to its internal functionality based on so called\u00a0<i>bit-blasting<\/i>, 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\u2019s 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\u00a0<a href=\"https:\/\/projects.informatik.uni-freiburg.de\/projects\/isat3\/\" target=\"_blank\" rel=\"noopener\">iSAT3<\/a>\u00a0rests upon a diverse technique, namely\u00a0<i>interval arithmetic<\/i>, 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 \u201ctransferred\u201d it from academia to industry.<\/p><p>In addition to random search, CBMC, and iSAT3, we have three more model checkers running in BTC Embedded<i>Platform<\/i>\u00a0and we are currently investigating some more promising candidates \u2013 to be optimally prepared for new customer requests.<\/p><figure class=\"content-image \"><\/figure>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-620c7ed elementor-widget elementor-widget-heading\" data-id=\"620c7ed\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Conclusion<\/h2>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-5539473 elementor-widget elementor-widget-text-editor\" data-id=\"5539473\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p>Coming back to the starting point of this article, i.e. the \u201c<i>serious gap between the needs of automotive code verification and open-source software model checker capabilities\u201d<\/i>, I have tried to explain why the commercial and customer-centric verification tool BTC Embedded<i>Platform<\/i>\u00a0performs so well in a real-world industrial setting. The authors of the case study recommend that \u201c<i>the software model checking community and industrial partners [\u2026] should [\u2026] set up a substantial set of industrial benchmarks<\/i>\u201d such that academia can also\u00a0<i>focus<\/i>\u00a0on real-world industrial problems. I absolutely appreciate such joint effort as this will lead to a gain for both sides:\u00a0<i>Academia<\/i>\u00a0can adjust their tools to industrial needs and thus increases the value of their research and\u00a0<i>industry<\/i>\u00a0can 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:<\/p><p>\u201c<i>If you chase two rabbits, you will not catch either one.<\/i>\u201d<\/p><p>With this in mind: Stay focused!<\/p><figure class=\"content-image \"><\/figure>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>1. Focus on effectiveness to solve the problem of your customer! Since day one we address exactly the problem  [&hellip;]<\/p>\n","protected":false},"author":5,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"elementor_theme","format":"standard","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"categories":[1],"tags":[60],"product":[],"use_cases":[],"class_list":["post-1675","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-model-checking"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/posts\/1675","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/comments?post=1675"}],"version-history":[{"count":10,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/posts\/1675\/revisions"}],"predecessor-version":[{"id":12544,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/posts\/1675\/revisions\/12544"}],"wp:attachment":[{"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/media?parent=1675"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/categories?post=1675"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/tags?post=1675"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/product?post=1675"},{"taxonomy":"use_cases","embeddable":true,"href":"https:\/\/www.btc-embedded.jp\/ja\/wp-json\/wp\/v2\/use_cases?post=1675"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}