电子发烧友网>电子资料下载>电子论文>自动控制系统论文>基于B方法的实时控制系统的容错设计

基于B方法的实时控制系统的容错设计

1846656 2009-08-28 | rar | 127 | 次下载 | 2积分

资料介绍

B 方法是形式化方法之一，支持软件开发的全部过程，它通过严格的数学推导和证明
来保证软件设计和代码的正确性。在现有的基本方法的基础上，要想进一步提高系统的可靠性，需要在软件开发中引入容错机制，使软件潜在的差错对可靠性的影响缩小到最低程度。
本文将B 方法应用于实时控制系统的容错设计，并通过变配电所的馈出实时控制系统这一实例的研究，阐述此方法从建立初始模型，精化到最终实现的开发步骤。
关键词：形式化方法；B 方法；容错设计
随着实时控制软件在可靠性和安全性要求极高的环境和系统中的广泛使用，对软件可靠
性的依赖正在以前所未有的速度增长。目前提高软件可靠性的一个重要的技术是容错设计。
本文将形式化B 方法应用于模型驱动的实时控制系统的开发中，逐步将容错机制例如故障检测，冗余技术和故障恢复融入到系统的规格说明和设计开发中。
B 方法是一种对软件系统进行描述、设计和编码的形式化方法[1][2]。B 方法产生于20 世
纪80 年代早期，在Z 语言的研究基础上引入了新的技术：谓词的转换和Dijkstra 的最弱前
置条件。它以一种基于Zermelo-Frankle 集合论的符号表示法来书写，使程序规格说明处于一个统一的数学框架下，减少了出现语义错误的可能性[3]。
本文通过变配电所系统这个实际项目的开发来说明容错控制系统的开发步骤，由于变配
电所系统涉及内容太多，为了便于分析，这里只考虑系统馈出（负载）的容错设计。项目开发用的是B_Core’s BToolkit 4.0，这个工具支持软件开发的全部过程，包括建立抽象机、精化和实现，语法分析，类型检查，大部分的正确性证明以及代码的自动生成。