SCODE方法

SCODE方法是由SCODE-ANALYZER支持和实现的。它能在系统设计中对工具标志错误的形式化验证,可以立即纠正。因此,开发人员总是可以在正式验证的系统上工作。专业人员可以利用这些结果优化现有的软件,设计新的软件,提高可测试性。

所有结果都可以通过其他工具(包括程序代码的自动生成)以及各种形式进行进一步处理。

SCODE方法

机电制动器的问题空间(例子)

SCODE方法是一个三步的迭代过程,它可以轻松显示和分析系统。它旨在把一个问题分解成为可以独立解决的小问题,并利用这些小问题的解决方案来解决主要问题。SCODE-ANALYZER引导用户完成整个过程并主动提供支持。

步骤1— 定义问题空间

第一步是定义问题空间,考虑系统的所有方面或导致系统发生变化的系统坏境(例如,用户干预,传感器的测量结果)。所引起的任何改变(如修改的变量或信号)都被视为输出。

步骤 2-定义模式

压缩制动卡钳模式的定义(例子)

在第二步中, 有效和无效的系统模式被描述。函数开发人员通过组合每个维度的选择选项来定义模式。

带有不同输入维度的相同输出规则

组合的不同输入规则可以生成具有相同输出维度的组合, 换言之, 不同的条目会导致系统中的相同的变化。

SCODE-ANALYZER提供支持并检查所有组合是否都被考虑到, 这样就不会忽略任何异常. 这样可以防止在开始时未定义所有要求时出现的后续和代价高昂的意外。此外, 软件还检查每个问题空间组合是否分配给单个模式, 并且在模式定义中没有重叠。

步骤3 -定义模式转换

模式转换的表和图形显示

在第三个步骤中, 函数开发人员定义系统在模式之间的转换时应如何反应。通过使用表或图形用户界面, 他们可以确定哪个事件导致了从一种模式到另一种方式的转换。它还可以确定某些模式之间的转换是无效的。开发人员以与完整、死锁和其他属性的模式相同的方式检查定义的事件。