论文部分内容阅读
轨道交通区域控制器是我国轨道交通信号系统选型的主流制式--基于通信的列车控制系统的核心子系统,其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是区域控制器自身的复杂性以及领域知识的繁杂难以掌握,使得形式化方法很难应用到安全需求的验证中去.针对这些问题,提出一种安全需求的自动验证方法,使用半形式化的问题框架方法来建模和分解安全需求,根据需求模型自动生成安全需求的验证模型和验证性质,在此基础上自动生成验证模型的Scade语言实现,并通过DesignVerifier验证器对需求进行组合验证.最后