SAT-based abstraction refinement for programmable logic controllers
SAT-based abstraction refinement for programmable logic controllers
复制标题
基于 SAT 的可编程逻辑控制器抽象细化
DOI：
10.1109/dcds.2011.5970325
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
S. Kowalewski
中科院分区：
文献类型：
--
作者：
Sebastian Biallas;Jörg Brauer;S. Kowalewski
本文研究了反例引导的抽象细化在指导列表中编写的程序中，作为模型检查框架的一部分。更重要的是，它提出了一种基于SAT解决的自动抽象细化的方法。该技术基于命题布尔逻辑中指令列表的语义的编码。由于优雅的想法和仔细的工程已经将SAT求解器提高到州，因此他们可以快速确定涉及数千个变量的结构性问题的满足性，因此这种方法在实践中缩放得很好。但是，该方法的真正力是对程序的语义的单一描述可用于在许多抽象域中执行抽象完善，包括但不限于间隔和位集，从而将细化从选择的抽象。
This paper studies the application of counterexample-guided abstraction refinement to programs written in Instruction List as part of a model checking framework. More importantly, it presents an approach for automatic abstraction refinement based on SAT solving. This technique is based on an encoding of the semantics of Instruction List in propositional Boolean logic. Since elegant ideas and careful engineering have advanced SAT solvers to the state they can rapidly decide satisfiability of structured problems that involve thousands of variables, this approach scales well in practice. The true force of this method, however, is that a single description of the semantics of a program can be used to perform abstraction refinement in a number of abstract domains, including but not limited to intervals and bit sets, thereby decoupling the refinement from the chosen abstraction.