CamFort: Automated evolution and verification of computational science models

CamFort：计算科学模型的自动演化和验证

• 批准号: EP/M026124/1
• 负责人: Andrew Rice
• 金额: $ 69.07万
• 依托单位: University of Cambridge
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2015
• 资助国家: 英国
• 起止时间: 2015 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FM026124%2F1
• 关键词: CamFort; Automated; evolution; verification; computational

Scientific models play a vital role in science and policy making. Many models are now expressed as complex computer programs which are often the result of decades of research and development, possibly involving multiple researchers or teams. This has lead to significant investment in maintaining these models and evolving them to use modern programming approaches or to work efficiently on new hardware platforms (such as cloud computing resources). However, the complexity of these models makes maintenance and evolution difficult. In particular, changing a complex model's code whilst ensuring it produces the same results is difficult; maintenance/evolution of complex models is often error prone. The complexity of a piece of software can be classified as either intrinsic or accidental. Intrinsic complexity is an essential reflection of the complexity inherent in the problem and solution at hand. Alternatively, accidental complexity arises from the particular programming language, design or tools used to implement the solution. Many of the research contributions of programming language design and software engineering have been aimed at reducing the accidental complexity of software. However, many of these approaches have not been targetted at scientific computing. There is now a need to develop these contributions so that they meet the needs of scientists. Addressing these needs will provide huge benefits to science and policy through increased productivity and trust in models. Our collaborations with leading research groups in science have highlighted the huge existing investments in established models. We are therefore aiming to support the evolution, rather than replacement, of existing code and working practices. Our goal is to apply cutting edge programming language and software engineering research to help develop "sustainable" software, which maintains its value over generations of researcher. Our focus is on models developed in the Fortran language, as this remains a dominant programming language in scientific computing, owing in part to its longevity. We will provide practical tools which scientists can use to reduce the accidental complexity of models through evolving a code base, as well as tools for automatically verifying that any maintenance/evolution activities preserve the models behaviour. We will develop new mechanisms for program comprehension and transformation in order to bring effective techniques from programming language design and software engineering across the chasm to scientific computing. Ultimately, reducing the effort to maintain and evolve code will free-up scientists to focus on the core aspects of the science, and will lead to models that are more easily communicated, disseminated, and reused between researchers, supporting core ideals of science.

科学模型在科学和政策制定中发挥着至关重要的作用。许多模型现在被表示为复杂的计算机程序，这些程序通常是数十年研究和开发的结果，可能涉及多个研究人员或团队。这导致在维护这些模型和发展它们以使用现代编程方法或在新的硬件平台（如云计算资源）上有效地工作方面进行了大量投资。然而，这些模型的复杂性使得维护和发展变得困难。特别是，改变一个复杂模型的代码，同时确保它产生相同的结果是困难的；复杂模型的维护/演化往往容易出错。一个软件的复杂性可以分为固有的和偶然的两类。内在复杂性是问题和解决方案内在复杂性的本质反映。另外，意外的复杂性来自于用于实现解决方案的特定编程语言、设计或工具。编程语言设计和软件工程的许多研究贡献都旨在降低软件的意外复杂性。然而，这些方法中的许多都不是针对科学计算的。现在有必要发展这些贡献，以满足科学家的需要。解决这些需求将通过提高生产力和对模型的信任，为科学和政策带来巨大的好处。我们与科学领域领先研究小组的合作凸显了对既定模型的巨大现有投资。因此，我们的目标是支持现有代码和工作实践的演进，而不是替代。我们的目标是应用尖端的编程语言和软件工程研究来帮助开发“可持续”的软件，这些软件在几代研究人员中保持其价值。我们的重点是用Fortran语言开发的模型，因为它在科学计算中仍然是一个主要的编程语言，部分原因是它的寿命长。我们将提供实用的工具，科学家可以使用这些工具通过进化代码库来减少模型的意外复杂性，以及自动验证任何维护/进化活动是否保留模型行为的工具。我们将开发新的程序理解和转换机制，以便将有效的技术从编程语言设计和软件工程跨越鸿沟引入科学计算。最终，减少维护和进化代码的工作将解放科学家，让他们专注于科学的核心方面，并将导致更容易在研究人员之间沟通、传播和重用的模型，从而支持科学的核心理想。

项目成果

Scrap Your Reprinter: A Datatype Generic Algorithm for Layout-Preserving Refactoring

废弃您的重印机：用于保留布局重构的数据类型通用算法

• 发表时间: 2017
• 作者: Clark H

Verifying spatial properties of array computations

验证数组计算的空间属性

• DOI: 10.1145/3133899
• 发表时间: 2017
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Orchard D

Behavioural Types: from Theory to Tools

行为类型：从理论到工具

• 发表时间: 2017
• 作者: Dominic Orchard

Combining effects and coeffects via grading

通过分级结合效应和协同效应

• DOI: 10.1145/2951913.2951939
• 发表时间: 2016
• 作者: Gaboardi M

Automatic Reordering for Dataflow Safety of Datalog

自动重新排序以确保数据记录的数据流安全

• DOI: 10.1145/3236950.3236954
• 发表时间: 2018
• 作者: Contrastin M