SHF: Small: Improving the Applicability of Haskell-Hosted Semi-Formal Models to High Assurance Development

在工程实践中，模型是理解如何构建复杂系统的重要组成部分。在这个项目中，高级模型和计算机系统的有效实现将在一个单一的框架下并行开发，该框架使用高度自动化来弥合它们之间的差距。这是可能的，由于使用现代函数语言的模型和实现，并部署了一个新的和强大的通用和半自动细化技术。函数语言Haskell已经享受了巨大的成功，作为一个平台，复杂系统的高级建模与它的抽象风格的语法，国家的最先进的类型系统，和强大的抽象机制。在这个项目中，Haskell将被用来表达一个半形式化的模型和一个高效的实现，采用两种不同的计算形式，具有相同的数学基础。该项目开发的工具和方法使用转换，如worker/wrapper转换来构建这些模型和实现之间的联系，降低安全内核和关键控制系统等应用领域的高可靠性软件和硬件组件的开发成本。降低将半正式规范和模型与实际实现联系起来的成本将产生巨大的影响。例如，通用标准的评估保证等级（EAL）5和6要求采用半正式的方法来构建此类链接，而本项目解决了这一要求的关键部分。

In engineering practice, models arean essential part of understanding how to build complex systems. Inthis project, high-level models and efficient implementations ofcomputer systems will be developed side-by-side under a singleframework that bridges the gap between them using a high degree ofautomation. This is possible due to the use of a modern functionallanguage for both the model and implementation, and the deployment ofa new and powerful general-purpose and semi-automatic refinement technology.The functional language Haskell has already enjoyed considerablesuccess as a platform for high-level modeling of complex systems withits mathematical-style syntax, state-of-the-art type system, andpowerful abstraction mechanisms.In this project, Haskell will be used to express a semi-formalmodel and an efficient implementation, taking the form of two distinctexpressions of computation with the same mathematical foundation.The project develops tools and methodologies that use transformations likethe worker/wrapper transformation to construct links between these modelsand implementations, lowering the cost of the development ofhigh-assurance software and hardware components in applicationareas like security kernels and critical control systems.Lowering the cost of linking semi-formal specifications and models toreal implementations will have considerableimpact. For example, Evaluation Assurance Level (EAL) 5 and 6 of theCommon Criteria call for semi-formal methods to construct such links,and this project addresses keys part of this requirement.