由Adacore

日期和时间

本次网络研讨会现已按需开放。
请完成注册。

事件类型

按需网络研讨会

演讲者

Moy亚尼克
SPARK产品经理，AdaCore

杆查普曼
董事- Protean Code有限公司

描述

已故的计算机科学家Edsger Dijkstra曾经说过一句名言:“程序测试可以用来显示错误的存在，但不能显示它们的缺失。”近年来，由于需要使软件“防弹”以应对日益复杂的需求和普遍存在的安全攻击，这一内在缺陷变得更加严重。测试只能到此为止。幸运的是，正式的程序验证为测试提供了一个实际的补充，因为它解决了安全问题，同时将测试的成本保持在可接受的水平上。

在可靠性最为重要的行业中，形式验证具有经过验证的跟踪记录，在可用的技术中，SPARK工具集具有突出的功能。它已经成功地用于开发高置信软件，包括航空航天、国防和空中交通管理。SPARK工具可以处理与关键系统相关的健壮性(没有运行时错误)和功能正确性(基于契约的验证)的特定需求，包括那些符合认证需求的系统。

在本次网络直播中，SPARK专家Yannick Moy和Rod Chapman将介绍SPARK解决方案的当前状态，并解释如何在您当前的软件开发过程中成功地采用它。

与会者将学习: