Research Initiation Award: Formal and Contextual Analysis of Software

9308726杰克逊不断发展的软件所要求的许多任务-维护、逆向工程、重组等-取决于分析。 大型程序混淆了任何手动分析的尝试，因此研究集中在自动分析程序的工具上。一般来说，已经提出了两种工具：基于知识的工具，可以将程序组件的属性与问题域中的概念相关联，以及类似编译器的工具，通过计算依赖关系，切片，模块层次结构等来确定组件之间的关系。 每种方法都有缺点。 基于知识的工具，因为他们只关联问题域的概念与组件非正式的，不能提供严格的分析;查询的答案往往更像是提示比健全的推论。类似编译器的工具局限于代码的低级分析，因此查询及其响应必须仅根据代码构造来制定。 这项工作结合了两种方法的一些优点。关键思想是上下文抽象。 用户指定程序组件和问题域概念之间的抽象关系。 通过在问题域术语中解释代码的属性，各种分析就成为可能。 因为抽象关系是形式化的，所以分析是严格的，并且可以包括例如部分验证。 ***

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. ***