基于Event-B与ADT的TACS形式化开发方法与验证

摘要： 为克服Event-B方法在开发全新一代列车自主运行控制系统（Train Autonomous Circumambulate System,TACS）中所出现的建模复杂性问题，提出将抽象数据类型（Abstract Data Types,ADT）实例化与Event-B相结合的方法，对TACS进行形式化开发和验证。首先，根据TACS的需求以及案例研究等相关内容，提取TACS的功能需求...