{"id":214,"date":"2017-12-24T15:57:00","date_gmt":"2017-12-24T14:57:00","guid":{"rendered":"https:\/\/kindsonthegenius.com\/blog\/2017\/12\/24\/verification-of-invariant-properties-by-bounded-model-checking\/"},"modified":"2020-08-22T14:44:32","modified_gmt":"2020-08-22T12:44:32","slug":"verification-of-invariant-properties-by-bounded-model-checking","status":"publish","type":"post","link":"https:\/\/kindsonthegenius.com\/blog\/verification-of-invariant-properties-by-bounded-model-checking\/","title":{"rendered":"Verification of Invariant Properties by Bounded Model Checking"},"content":{"rendered":"<div style=\"color: #555555; font-size: 18px; line-height: 30px; text-align: justify;\">\n<div style=\"font-family: 'segoe ui';\">Bounded model-checking is a technique applied in handling of large state space problems.<br \/>The basic principle of bounded model-checking is that&nbsp; we do not handle the state space all at once. The checking is performed by&nbsp; restricting the length of the paths.<br \/>Partial verification can then be carried out within a given bound that consists of path of a definite length. The length of the paths can then be iteratively increased to accommodate more areas in the state space.<\/p>\n<p><i>Diameter of the State Space<\/i> can be defined a the length of the longest loop-free path. Therefore a checking a bound that is equal to the diameter of the state space would result in a complete check.<\/p>\n<p><b>Approach and Goals<\/b><br \/>The approach to bounded model checking problem is to map the problem to an appropriate SAT problem.<br \/>A model checking problem consists of a model and a property.<\/p>\n<p><i>Model<\/i>: Paths of bounded length are mapped onto boolean formula based on a characteristic function which takes into consideration the initial state and the State transition.<br \/><i>Property<\/i>: Invariant properties are mapped to Boolean formula as a characteristic function of that formula for all possible states<\/p>\n<p>The Boolean formula would evaluate to either true or false such that:<br \/>If the SAT solver does not find a substitution in the formula, then the property holds true<br \/>But if the SAT solver finds a substitution for the formula, then the substitution induces counterexample for that property.<\/p>\n<p><b>How to Describe a Path of Bounded Length<\/b><br \/>Beginning from the initial states: choose a characteristic function, say L(s) where s is the state<br \/>Transit along potential transitions: s0 &gt; s1 &gt; s2 &gt; s0 &gt;&#8230;.<br \/>The characteristic function is Cr(s0, s1) for path between s0 and s1<\/p>\n<p><i>How to Describe the Property<\/i><br \/>Another characteristic function p(s)<\/p>\n<p><b>Summary of Bounded Model Checking<\/b><\/p>\n<ul>\n<li>Bounded Model checking is applied in checking invariant properties<\/li>\n<li>It is very efficient in loop-free paths<\/li>\n<li>If there is a counterexample up to a certain bound, it could be found<\/li>\n<li>Handling Large State Space<\/li>\n<li>SAT solver: this is a symbolic technique that uses Boolean formulas<\/li>\n<li>For up to a given length of paths, only a partial result is obtained<\/li>\n<li>Can be used for test-case generation<\/li>\n<li>Tools that can be used:<\/li>\n<li>Symbolic Analysis Laboratory(SAL)<\/li>\n<li>SAL sal-alg used for automatic test generating<\/li>\n<li>CBMC: bounded model checker for C source code <\/li>\n<\/ul>\n<p><\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Bounded model-checking is a technique applied in handling of large state space problems.The basic principle of bounded model-checking is that&nbsp; we do not handle the &hellip; <\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_mi_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0},"categories":[359],"tags":[],"_links":{"self":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/214"}],"collection":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/comments?post=214"}],"version-history":[{"count":1,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/214\/revisions"}],"predecessor-version":[{"id":1495,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/214\/revisions\/1495"}],"wp:attachment":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/media?parent=214"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/categories?post=214"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/tags?post=214"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}