为克服Event-B方法在开发全新一代列车自主运行控制系统(Train Autonomous Circumambulate System,TACS)中所出现的建模复杂性问题,提出将抽象数据类型(Abstract Data Types,ADT)实例化与Event-B相结合的方法,对TACS进行形式化开发和验证.首先,根据TACS的需求以及案例研究等相关内容,提取TACS的功能需求和安全需求,并将功能需求和安全需求以非形式化的语言进行描述;然后,根据TACS的功能需求和安全需求进行模型精化层次的设计,避免因在抽象模型中建模复杂的需求而导致证明困难;最后,在模型中使用形式化语言Event-B对TACS的功能需求和安全需求进行建模并验证其正确性,且在建模过程中,利用ADT的抽象概念将轨道网络、轨道区域以及移动授权(Movement Authority,MA)等复杂系统组件在初始模型中指定组件的必要属性,且在后续系统建模过程必要的精化阶段引入组件的具体定义,以降低系统开发和证明的复杂度.结果表明:提出的方法有助于在早期开发阶段减少TACS中复杂的细节部分,使得证明义务成功率为100%,自动证明成功率占比83%,手动证明成功率仅占比仅17%,在简化证明义务的同时有效提高了自动化证明的占比.
To address the complexity challenges encountered in the development of the Train Autonomous Circumambulate System(TACS)modeling using the Event-B method,a methodology combining the instantiation of Abstract Data Types(ADT)with Event-B is proposed for the formal development and verification of TACS.Firstly,functional and safety requirements of TACS are extracted based on its requirements and relevant contents including case studies,which are described in non-formalized language.Subsequently,to avoid the difficulty in proving caused by complex modeling requirements in abstract modeling,a hierarchical design of the modeling refinement levels is conducted based on the TACS functional and safety requirements.Finally,the functional and safety requirements of TACS are formally modeled and verified using formal Event-B language.During the modeling process,the abstract concepts of ADT are employed to specify the essential attributes of complex system components,such as the track network,track regions,and Movement Authority(MA),in the initial model.Specific definitions of those components are introduced in subsequent refinement stages,reducing the complexity of system development and proof.The results indicate that the proposed approach helps reduce the complexity of intricate details in TACS during the early development stages,resulting in a 100%success rate in proving obligations.Furthermore,the success rate of automated proof accounts for 83%,while that of the manual proof is only 17%,simplifying the proof obligation while effectively increasing the proportion of automated proofs.