CAJ | 학술논문

为降低形式化建模的难度，本文深入研究了基于Event-B的开发框架，并结合控制系统中控制器与被控环境之间的交互特征，提出了一套基于Event-B的控制系统有序模块化建模指导原则，能够帮助设计人员在开发的早期更加深入地理解系统需求，获得清晰的建模思路和开发策略，为设计高安全性的软件系统提供保障。最后，应用该方法完成了RBC （区域控制器）系统的形式化建模，说明了该方法的实用性。
위강저형식화건모적난도，본문심입연구료기우Event-B적개발광가，병결합공제계통중공제기여피공배경지간적교호특정，제출료일투기우Event-B적공제계통유서모괴화건모지도원칙，능구방조설계인원재개발적조기경가심입지리해계통수구，획득청석적건모사로화개발책략，위설계고안전성적연건계통제공보장。최후，응용해방법완성료RBC （구역공제기）계통적형식화건모，설명료해방법적실용성。
In order to reduce the difficulty of formal modeling , this paper researched the developing frame of Event-B method in depth , combined it with the feature of interaction between controller and environment in control system , and proposed an ordered and modularized Event -B modeling instruction based on the combina-tion.It can help developers to get deeper understanding of the system requirement and a clear modeling and de -veloping tactic in the early stage of development , which guarantees for the designing of a high -safety software system.At last, the instruction was applied to the development of RBC system .Through this process of the Event-B modeling , the practicability of the method was showed .