Bonsai: Cutting Models Down To Size
PERSPECTIVES OF SYSTEM INFORMATICS, PSI 2014(2015)
摘要
In model checking, abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on multi-valued model checking can distinguish conclusive and inconclusive results, while increasing precision over traditional two-valued over-and under-abstractions. This paper describes the theory and implementation of multi-valued model checking for Promela specifications. We believe our tool Bonsai is the first four-valued model checker capable of multi-valued verification of parallel models, i.e. consisting of multiple concurrent processes. A novel aspect is the ability to only partially abstract a model, keeping parts of it concrete.
更多查看译文
关键词
Multi-valued Model Checking, Promela Specification, Abstract Destination States, Guarded Term, Quasi Boolean Algebra
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要