Step into the formal world with ease!

What if your PC could understand your requirements?

BTC 形式测试套件

借助 BTC SUP 形式语言,让您轻松步入到形式世界

ISO26262和 IEC61508标准推荐的使用准形式化和形式化记述方法(形式语言)来记述安全关键需求,但是形式语言比如 LTL有两个问题,第一是太难,不好学,第二是和自然语言需求的追溯性无法得到保证。BTC SUP 形式语言很好的解决了以上两个问题,她提供了一个任何人都可以快速入门的形式语言模板来帮助用户对安全关键需求轻松地进行准形式化和形式化。

 

形式化需求 = 更好的需求

在书写需求时,一般采用非形式化的自然语言来记述,需求的管理一般在 IBM DOORS 或 PTC Integrity 中进行管理。由于自然语言一般会有错误解释的空间,从而导致开发或测试工程师开发出并不是预期的算法。通过 BTC SUP 形式语言对自然语言的需求进行形式化以后,需求变得更加清晰,无歧义,计算机可以理解,从而提高需求本身的品质,并在随后的开发和自动测试流程中发挥威力。

 

如何使用 BTC SUP 形式语言进行形式化

您只需要三部就可以完成对自然语言需求的形式化操作。第一步,选取自然语言的关键词或短语做成宏定义,第二步,把宏定义按照 BTC SUP 的模板进行结构化,并定义时间约束。第三步,把宏定义关联到真实的被测系统的接口变量,从而完成全面的形式化,这时计算机也就可以理解您的需求了。

 

需求覆盖率的有效定义

在传统测试中,由于计算机不能理解需求,测试用例对于需求的覆盖程度是由工程师经验而决定的,需求的覆盖率的判定由于人的理解不同而不同。

对于BTC SUP 形式化后的需求,由于计算机可以理解需求,从而可以全自动地定量的数学计算出需求的覆盖程度,作为一个重要数据指标来评估测试的完整性。

形式化需求 = 更好的验证

形式化需求可以用于以下自动测试及验证,来显著提高产品的品质: