XiaoMi-AI文件搜索系统
World File Search System形式化
面向对象软件的形式化验证 2010 - KIT
本卷包含在 2010 年 6 月 28-30 日于法国巴黎举行的面向对象软件形式化验证国际会议 (FoVeOOS 2010) 上发表的受邀论文、研究论文、系统描述、案例研究和立场文件。会后，选定论文的修订版将在 Springer 的计算机科学讲义系列中出版。形式化软件验证已经超出了学术案例研究的范畴，工业界也对此表现出浓厚的兴趣。下一个合乎逻辑的目标是工业软件产品的验证。工业实践中使用的大多数编程语言都是面向对象的，例如 Java、C++ 或 C#。FoVeOOS 2010 旨在促进该领域研究人员之间的合作与互动。FoVeOOS 由 COST Action IC0701 ( www.cost-ic0701.org ) 组织，但它超出了该行动的框架。会议向整个科学界开放。所有提交的论文都经过同行评审，在 35 篇提交的论文中，程序委员会选择了 23 篇在会议上展示。我们衷心感谢所有提交作品供审议的作者。我们还要感谢程序委员会成员以及其他审阅者在审查和选择过程中付出的巨大努力和专业工作。他们的名字列在以下页面中。除了贡献的论文外，F
形式化方法及其在数字 SY 主干验证中的作用...
本报告基于 FAA 数字系统验证手册（帮助 FAA 认证专家解决高级技术问题的指南）的一章。其目的是解释在软件和硬件要求、设计和实施的规范和验证中使用形式化方法，确定将这些方法应用于关键应用中使用的数字系统的优点、弱点和困难，并提出在提供形式化方法支持认证时需要考虑的因素。本演示集中于形式化方法的基本原理及其对关键应用保证的贡献，例如在 DO-178B（民用飞机上使用的软件指南）2 提供的环境中；它旨在为那些不熟悉这些主题的人提供入门。配套报告提供了关于形式化方法的更技术性的讨论。~
形式化方法与关键系统认证
本报告主要面向 FAA 认证人员撰写，不要求认证人员之前接触过形式化方法。但是，它不是形式化方法教程：它包含大量关于形式化方法的优势、劣势和技术问题的讨论，这些问题应在认证中考虑，但并未解释如何使用形式化方法。报告中散布着一些简单的例子，但这些例子仅供大家感受所讨论的主题，并不代表认证中可能提供的特定技术或符号。那些希望提供形式化方法来支持认证的人显然必须成为他们所选方法的专家，认证人员同样需要获得所采用的特定方法的专业知识。第 2.8 节为开始此类研究的人提供了一些阅读建议。
形式化方法和关键系统的认证
本报告主要为 FAA 认证人员撰写，假设他们之前没有接触过形式化方法。但是，它不是形式化方法教程：它包含大量关于形式化方法的优势、劣势和技术问题的讨论，这些问题应在认证中考虑，但并未解释如何实施形式化方法。报告中散布着一些简单的例子，但这些例子仅供大家感受所讨论的主题，并不代表可能为支持认证而提供的特定技术或符号。那些希望提供形式化方法来支持认证的人显然必须成为他们所选择方法的专家，认证人员同样需要获得所采用的特定方法的专业知识。第 2.8 节为那些开始进行此类研究的人提供了一些阅读建议。
并发程序的形式化规范与验证
被认为可以降低开发的总成本。也就是说，它们必须被视为可以降低最终错误的数量，并且如果不进行这些操作，则感知成本必须高于执行这些操作的成本。。首先，讨论关于并发程序的人们可能希望能够证明什么。然后，提出了一个与这种功利主义观点一致的观察结果。这些在对系统规范的覆盖范围上有所不同，有些可以用作设计系统功能的基础。也就是说，程序的正式规范。接下来，编写正式规范的行为只是为了证明所作的决策与程序规范之间的一致性。最后，值得注意的是，其中一些技术在第一次验证尝试之前就已经与自动化工具（如验证器）相关联，目的是获得正确的系统功能。