B方法在配电自动化系统中的应用研究

摘要

在现代科学技术的推动下，配电自动化领域有了突飞猛进的发展。虽然取得了不少的研究成果，但是仍然存在着诸多问题。目前的配电自动化系统无法进行严格的检查，其代码的正确性只能依靠测试，但经过测试后并不能说明软件中不存在错误。形式化方法可以有效地解决这类问题。B方法是形式化方法的一种，它是建立在严格数学基础之上的软件开发方法，提供了一个统一的数学框架，通过一系列证明义务，来证明系统构造的正确性，进而保证实现的系统具有高安全性、可靠性。
　　 鉴于以上情况，本文主要做了以下工作：
　　 1.介绍B方法的研究现状并对B方法的相关理论做了较为深入的学习，主要包括B方法的数学知识、开发软件的各个阶段、证明技术、以及对B工具的比较分析等。
　　 2.结合配电自动化系统的特点，设计了系统模型，并进行了模型的抽取。用B方法构建了实数抽象机、复数抽象机、节点抽象机、电流监控器及系统控制器，同时部分抽象机进行了精化和实现。由于馈线远方终端FTU不确定性，在此引入了PB(ProbabilisticB)。
　　 3.以REALTYPE、CONTROLLER抽象机为例，进行了正确性证明，得到了实验结果，并指出了在下一步的研究中需要完善的问题。

目录

文摘

英文文摘

声明

第一章绪论

1.1研究背景及意义

1.2课题的研究现状

1.3本文研究的主要内容及组织结构

第二章B方法的相关理论

2.1 B方法基本数学知识

2.1.1广义代换

2.1.2二元关系

2.1.3自由性与非自由性

2.1.4 B类型

2.2 B抽象机

2.2.1静态行为

2.2.2动态行为

2.3精化/实现

2.4 B方法的证明理论

2.4.1抽象机的正确性证明

2.4.2精化的正确性证明

2.4.3实现的正确性证明

2.5 B工具

2.6小结

第三章配电自动化系统模型

3.1可靠性影响因素

3.2系统分析

3.3非形式的规范

3.4小结

第四章B方法在配电自动化系统中的应用研究

4.1构造复数

4.1.1实数抽象机

4.1.2复数抽象机

4.1.3抽象机的精化与实现

4.2节点抽象机

4.3电流监控器

4.4系统控制器

4.4.1 CONTROLLER抽象机

4.4.2 CONTROLLER实现

4.5小结

第五章系统的正确性证明

5.1 REAL_TYPE正确性证明

5.1.1类型检查

5.1.2证明义务

5.2 CONTROLLER正确性证明

5.2.1类型检查

5.2.2证明义务

5.3 Atelier B的实验结果

5.4小结

总结与展望

本文的工作总结

将来的工作展望

致谢

参考文献