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

点击翻译按钮获取中文摘要

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.