论文摘要
形式化B方法建立在严格的数学基础上,通过严格的验证技术证明其正确性,尤其对大型复杂系统的描述是非常有用和正确的。它是一种详细规格说明、设计和系统编码的方法。通过B方法来描述和验证能发现其它方法不易发现的系统描述不一致、不明确或不完整性,有助于增加软件开发人员对系统的理解。实践经验告诉我们使用形式化方法的系统设计过程中主要的瓶颈问题就是验证,形式化方法的验证方法主要有定理证明和模型检测。定理证明就是从系统的公理出发使用推理规则逐步推导出其所期望特性的证明过程。证明所需要的步骤依赖于系统的公理和推理规则。文中首先对免疫因子网络的机器进行了定理证明,从而保证了机器的正确性。模型检测则是对有限状态系统空间进行穷尽搜索。其主要方法为使用形式化描述语言或直接使用迁移系统等对系统进行建模,然后进行自动化的连贯性检查。这允许检查遍及机器的所有可及的状态,使用相应的算法在有穷步内自动检测出待检测系统是否满足待检测性质。模型检测的主要缺点是状态空间爆炸问题。虽然状态空间爆炸问题已经得到一些缓解,但是一方面,由于系统自身内在的非确定特性,当系统所包含的可相互通讯的子系统数目较多时,整个系统规模不可避免的会增大;另一方面,系统所包含的数据类型有较大的值域时,不同的取值组合也会产生较多的状态。无论是子系统的组合还是数据域的组合,都使整个状态空间呈指数增长。条件分析是一种考虑了输入条件之间的关系,探究输入变量的组合的生成状态空间的方法。我们提出将条件分析方法应用在缓解状态空间爆炸的问题上,该过程对需求的语义进行检查,并将输入和输出之间或输入和转换之间的关系重新表述为逻辑关系对状态空间进行删减。它考虑了输入条件之间的关系,得到的状态空间数目大大减少,从而缓解了状态空间爆炸问题。精化是B方法中的关键性概念。它是从高层次的规格说明开始逐步精化到实现,最后的实现可以自动地翻译成可执行的代码。精化的模型最终被精化到具有充足的实现细节。精化模型保证在抽象机的连续精化步骤过程中,被定义的每个不变式和前置条件都满足。操作、不变式和前置条件生成一系列证明义务。本文对因子网络的机器进行了精化,变换到另一种更具体的数学模型,减少了非确定性。文章最后是系统的最后代码实现。