Research Initiation Award: Formal and Contextual Analysis of Software

[308726] Jackson软件开发中的许多任务——维护、逆向工程、重构等——都依赖于分析。大型程序会干扰任何手工分析的尝试，因此研究集中在自动分析程序的工具上。一般来说，已经提出了两种工具：一种是基于知识的工具，它可以将程序组件的属性与问题领域的概念关联起来；另一种是类似编译器的工具，它通过计算依赖关系、切片、模块层次等来确定组件之间的关系。每种方法都有缺点。基于知识的工具，因为它们只是非正式地将问题领域概念与组件联系起来，不能提供严格的分析；对问题的回答往往更像是提示，而不是声音推断。类似编译器的工具仅限于对代码进行低级分析，因此查询及其响应必须仅根据代码构造进行表述。这项工作结合了这两种方法的一些优点。关键思想是上下文抽象。用户指定程序组件和问题域概念之间的抽象关系。通过在问题领域术语中解释代码的属性，各种分析成为可能。由于抽象关系是形式化的，因此分析是严格的，并且可以包括，例如，部分验证。＊＊＊

9308726 Jackson Many of the tasks demanded by evolving software-maintenance, reverse engineering, restructuring, etc.-depend on analysis. Large programs confound any attempt at hand analysis, so research has focused on tools that analyze programs automatically. Broadly speaking, two kinds of tools have been proposed: knowledge-based tools that can associate properties of program components with notions from the problem domain, and compilerlike tools that determine relationships among components by calculating dependencies, slices, module hierarchies, etc. Each approach has disadvantages. The knowledge-based tools, because they only associate problem domain notions with components informally, cannot provide rigorous analysis; answers to queries tend to be more like hints than sound inferences. The compiler-like tools are confined to low- level analysis of the code, so the queries, and their responses, must be formulated in terms of code constructs alone. This work combines some of the advantages of both approaches. The key idea is contextual abstraction. The user specifies an abstraction relationship between program components and problem domain notions. A variety of analyses then becomes possible by interpreting properties of the code in problem domain terms. And because the abstraction relationship is formal, the analyses are rigorous and can include, for example, partial verification. ***