安全关键的信息物理系统中时序行为的组合与精化

信息物理系统（cyber physical systems, CPS）通常被应用于安全关键的场景中，需要进行实时监控，并计算反馈信息，实现对外部环境的自动控制与管理.基于模型驱动的开发方法是针对实时的、异构的CPS进行开发的，而模型的可组合性是其中的核心关键点.针对时序行为的可组合问题，首先通过时序约束语言（clock constraint specification language, CCSL）建立系统的时序行为需求模型，在此基础上通过迁移系统描述CCSL的时序行为语义，并给出其组合操作方法及可组合性的形式化定义.进一步地，对时序行为进行精化操作，给出从时序行为需求模型到任务执行模型的转换方法.同时，基于L*方法对模型行为进行学习，实现组合验证以缓解状态爆炸问题，并验证精化后模型的可组合性.最后通过仿真实验及主从智能小车实例对精化与验证方法进行评估.相关数据显示，精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.