Grafting a Promela front-end with abstract data types to mitigate the sensitivity of (compositional) analysis to implementation choices

研究成果: 雜誌貢獻會議論文同行評審

1 引文 斯高帕斯(Scopus)

摘要

Recently, an active research topic in software verification is applying model checkers to programs, such as multi-threaded Java code. However, a program typically consists of more behaviors, such as operations on complicated data structures or implementation details which are typically made for some criteria like performance. A brute-force model extraction may produce a poor model for analysis engine. In this paper, we give examples to show how subtle changes in implementation may result in considerable differences in analysis, particularly to compositional analysis. Unfortunately, these implementation choices are made by programmers - people who typically do not possess the knowledge of verification. To mitigate such sensitivity, we advocate that verification tools should recognize and support abstract data types and, in the meantime, prohibit or suppress the use of array. Programming process behaviors with abstract data types can hide and converge the implementation choices. More importantly, abstract data types are informative. They provide essential information for tool automation to select a best implementation for analysis. In this paper, we describe the design and implementation of such a prototype tool which can parse systems written in Promela syntax.

原文???core.languages.en_GB???
頁(從 - 到)139-153
頁數15
期刊Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
3639
DOIs
出版狀態已出版 - 2005
事件12th International SPIN Workshop on Model Checking Software - San Francisco, CA, United States
持續時間: 22 8月 200524 8月 2005

指紋

深入研究「Grafting a Promela front-end with abstract data types to mitigate the sensitivity of (compositional) analysis to implementation choices」主題。共同形成了獨特的指紋。

引用此