基于时间自动机的RBC控车场景建模与验证的任务书任务书：基于时间自动机的RBC控车场景建模与验证一、任务描述在铁路列车的行车控制系统中，RBC（RadioBlockCenter）是必不可少的一个组成部分。RBC控制着车辆的行进，使车辆保持安全的车距，并控制车辆的速度等参数。为了确保系统的安全性和可靠性，需要对RBC进行建模和验证。本次任务的目标是基于时间自动机，对RBC控车场景进行建模，并用模型检测工具对模型进行验证。具体任务分为以下两个部分：1.基于时间自动机的RBC控车场景建模：（1）根据列车行车控制系统中的RBC控车场景，建立模型。（2）使用时间自动机的理论和工具，将模型进行形式化描述。2.对模型进行验证：（1）使用模型检测工具，对模型进行验证。（2）根据验证结果进行分析和总结，找出模型存在的问题，并提出改进方案。二、任务要求1.对列车行车控制系统中的RBC控车场景进行了解，熟悉时间自动机的理论和工具。2.熟练掌握模型建立和验证技能，具有良好的数学基础和逻辑思维能力。3.任务完成后需要完成一份详细的实验报告，包括模型建立过程、验证结果分析和总结、改进方案等内容。4.任务要求在规定时间内完成。三、参考文献1.J.Sifakis.Thesymbolcracyapproach.InG.Plotkin,C.Stirling,andM.Tofte,editors,Proof,LanguageandInteraction,pages637–657.MITPress,2001.2.O.MalerandD.Nickovic.Monitoringtemporalpropertiesofcontinuoussignals.In22ndInternationalConferenceonComputerAidedVerification(CAV’10),pages542–550,Berlin,Heidelberg,2010.Springer.3.Y.Chen,S.Huang,X.Du,andH.Li.Atimeautomatabasedobstacleavoidancemethodforhighspeedtrains.JournalofIntelligent&RoboticSystems,1-11,2019.四、预期成果1.完成RBC控车场景建模和时间自动机形式化描述，并使用模型检测工具对模型进行验证的任务。2.撰写详细的实验报告，包括模型建立过程、验证结果分析和总结、改进方案等内容。3.对任务执行过程中存在的问题和困难进行总结，并提出对策和改进建议。五、时间安排任务完成期限为一个月。具体安排如下：第一周：了解相关背景知识，确定建模方法。第二周：完成RBC控车场景建模工作。第三周：完成时间自动机形式化描述工作。第四周：使用模型检测工具进行模型验证，撰写实验报告。六、评价标准根据任务完成情况和实验报告质量进行评价。1.任务完成情况：包括模型建立和验证的质量，是否达到要求等方面。2.实验报告质量：包括实验报告的结构、内容是否详实、分析是否有深度、写作是否清晰、文字描述、排版美观等方面。3.根据实验报告中提出的改进方案是否可行和有效性进行评价。