当前位置：首页> 形式化需求描述

形式化需求描述

时间：2023-03-31 18:59:49 下载该word文档

航空电子领域中基于形式化方法的安全需求描述
1.基于形式化方法的安全需求描述意义和准则
在许多领域软件系统的安全性与可靠性显得日益重要，尤其在对安全性和可靠性要求极高的综合航空电子领域中软件系统的安全性和可靠性更显重要。因为综合航空电子系统对于整个飞机的安全性起着至关重要的作用。然而，伴随着航电系统日益增长的复杂性和系统集成的问题依然会增加潜在的错误并可能直接影响到飞机的安全性和可靠性。传统的软件工程方法已经很难满足这样复杂和安全性要求极高的需求，这迫切需要新的方法来设计开发安全性更高，资金时间投入更少的系统,为了解决这些实际问题，基于模型的开发方法（MBD）被引入，通过对需求描述严格的形式定义，可执行的原型设计，定理证明，模型检测，和高质量代码的自动生成等形式化技术大大提升了系统的安全性和可靠性，同时也大大节省了时间和成本。
大多软件开发的错误源于需求分析阶段的逻辑错误。这些逻辑错误会传递到软件开发的后续阶段，大量的重复工作花费在修补由于需求阶段的逻辑错误而导致的系统错误。而且，需求错误往往是相当严重的错误。需求阶段的错误比设计或实现阶段所引入的错误更加影响系统的安全性。
发现错误的一个有效途径就是创建一个系统外部可见行为的精确且可执行的系统模型。为了建立可读的且数学形式上的精确的系统功能行为模型，已经有多种符号语言被开发出来。比较出名的有SCR,RSML,SpecTRM,和Statecharts。基于这些符号语言来创建模型能够发现大量系统描述中的错误。而且能够作为与用户交互的实模型，并能够类仿真的形式向客户执行。最好的情形就是经过精心设计的符号语言能够支持系统模型的自动形式化安全分析（如图1.1）。它使得通过一致性和完备性检查来发现错误成为可能，同时有能

力来检查应用程序建模的一些性能描述。总之，创建系统行为的精确模型不仅仅使得能够在系统生命期尽早地发现错误，并及时地解决，还能够提升后续的系统设计，编码，验证，测试的质量。

图1.1基于形式化方法的安全性分析
系统需求描述作为系统开发的蓝图，它应该是对系统期望行为的完备的，一致性的，精确的描述。否则将会把不安全因素带进后续的设计、编码、测试等环节，将严重影响系统的安全性能同时也增加更多的开发代价。所以提供方法和技术使尽可能早地排除与需求相关的错误显得非常重要。
为了分析和发现需求描述的错误，描述语言所应具有的一些标准对于我们达到我们的目标至关重要。准则一是需求描述语言只详细描述系统的黑盒行为而不包括内部的设计信息；准则二是描述语言要让在保证形式化的准确性的同时能够方便专业技术人员和非专业人员易读易理解建立起他们对系统统一的认识；准则三，就是要具有描述复杂系统的能力，在这里主要借鉴了Harel所提出的“clustering“的概念，另一方面也用到了Harel“abstraction”思想；其他两个标准是最小性和简洁性。最小性就是需求描述仅包含对开

阅读全文