来自欧洲ProCoS项目的经验：可证明正确的系统

《Formal Aspects of Computing》：Experiences from the European ProCoS Projects: Provably Correct Systems

本文回顾了1990年代欧洲ESPRI ProCoS项目，探讨其在形式化方法领域的贡献，包括Duration Calculus和Unifying Theories of Programming的发展，分析其对系统正确性和硬件验证的影响，并总结项目对后续研究及参与者职业发展的影响。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

本文介绍了欧洲ESPRIT ProCoS项目中关于“可证明正确系统”的合作项目，以及20世纪90年代的相关倡议。还讨论了这些项目在形式化方法领域的影响。文章提供了这些项目的一般概述，并收录了参与者的回忆，包括这些项目对参与者后续职业生涯的影响。这些项目解决了在不同形式化层次上连接形式化方法的问题，包括需求、规范、编译，甚至直接到机器代码以及硬件。研究基于编程语言Occam的一个代表性子集，后来Occam语言增加了反映特定编译问题的元素，而这些元素在Occam原语言中并不存在；同时，还涉及了相关的Transputer微处理器。实际上，这些项目之后最重要的、最具持久影响力的成果是“持续时间演算”（Duration Calculus）和“统一编程理论”（Unifying Theories of Programming），这两个都是形式化方法的分支领域，并拥有各自的研究者和实践者社区。

人工智能摘要

人工智能生成的摘要（实验性)

此摘要是使用自动化工具生成的，并非由文章作者撰写或审核。它旨在帮助读者发现文章的相关性，并协助来自相关研究领域的读者理解文章内容。它是对作者提供的摘要的补充，作者提供的摘要仍然是文章的官方摘要。完整文章才是权威的版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的摘要版本。

要查看此由人工智能生成的通俗语言摘要，您必须具有高级访问权限。