写于 2018-12-26 05:05:04| 澳门金沙网站网址| 体育
<p>计算机崩溃和软件错误令人愤怒 - 通常是迟来的 - 教会我们定期备份的价值</p><p>但他们可能成为过去吗</p><p>我们都去过那里:几天或几周的工作瞬间毁灭了</p><p>它可能是一个崩溃的文字处理器,一个崩溃的操作系统,计算机吃你的功课,破坏你的实验室结果,你的报告......但是如果软件不仅仅是数据呢</p><p>如果你的钱或你的生活依赖于一个特定的软件没有失败怎么办</p><p>证券交易所和银行系统由软件控制,每当你开车或上飞机时,你就把生命交给软件系统</p><p>当然,安全关键系统的构建比普通软件更加谨慎,但仍然会出现错误</p><p>错误测试 - 当今使用的主要软件保障方法 - 存在以下问题:不再发现任何错误并不意味着它们不存在</p><p>也许你只是看起来不够长或太难</p><p>那么我们能做些什么呢</p><p>那么,还有另一种方法:“正式验证”</p><p>从本质上讲,软件只是一种逻辑形式</p><p>使用数学证明,您可以证明一个软件将始终以某种方式运行</p><p>这个过程称为形式验证,可以显示一个软件中没有错误,但该技术有其自身的局限性</p><p>到目前为止,将这种方法直接应用于任何真正复杂的代码已经太困难了</p><p>这就是我们来自NICTA和新南威尔士大学的团队所做的:我们已经证明了一个复杂,关键的代码片段seL4微内核的正确性的正式证明</p><p> (微内核是一个最小的操作系统(OS)内核,可控制计算机硬件和操作系统其余部分的内存访问</p><p>)大约10,000行代码,seL4的大小是关键软件的典型代码,即使它很小对于操作系统(例如,Linux是数百万行代码)</p><p> seL4的主要工作是提供故障隔离:如果两个组件在微内核上运行 - 例如用户界面和医疗传感器 - 并且用户界面崩溃,则医疗传感器将不受影响</p><p>这是管理软件错误的一个很好的策略:如果你不能完全消除它们,至少要把它们包含在烦人但不致命的地方</p><p>虽然没有最终保证特定计算机系统能够正确运行我们的代码,但我们已经能够显着增加我们可以放入seL4大小的软件中的信任量</p><p> 30多年来,人们一直致力于实现这样的目标,现在终于成为现实</p><p>如果一切顺利,第一个基于seL4构建的商业产品最早可能会出现在2012年</p><p>这项技术有一系列的潜在用途,包括开发:但是当我们忙于尝试将这些代码推广到商业应用程序时,请记住你可以避免(一些)烦人的故障和崩溃的麻烦:

作者:公孙佩鲍