安全关键的信息物理系统中时序行为的组合与精化陈博1李曦1,2周学海1,21（中国科学技术大学软件学院江苏苏州215123）2（中国科学技术大学计算机科学与技术学院合肥230051）（chenbo2008@ustc.edu.cn）CompositionandRefinementofTimingBehaviorinSafety-CriticalCyberPhysicalSystemsChenBo1,LiXi1,2,andZhouXuehai1,21（SchoolofSoftwareEngineering,UniversityofScienceandTechnologyofChina,Suzhou,Jiangsu215123）2（SchoolofComputerScienceandTechnology,UniversityofScienceandTechnologyofChina,Hefei230051）AbstractCyberphysicalsystems(CPS)areusuallyusedinsafetycriticalscenarios,whichrequirereal-timemonitoring,computethefeedbackdata,andrealizeautomaticcontrolandmanagementoftheexternalenvironment.Modeldrivendevelopmentmethodisthemainwaytodevelopreal-timeandheterogeneousCPS,andthecomposabilityofthemodelisthekeypoint.Inthispaper,thetimingbehaviorspecificationmodelofthesystemisestablishedbytheclockconstraintspecificationlanguage(CCSL),andonthisbasis,thetimingbehaviorsemanticsofCCSLisdescribedbythetransitionsystems,anditscompositionoperationmethodandtheformaldefinitionofcomposabilityisgiven.Further,thetimingbehaviorisrefined,andthetransformationmethodfromthetimingbehaviormodelofspecificationtothetaskexecutionmodelisgiven,Thetimingconstraintbehavioratthespecificationlevelistransformedintothetimingconstraintbehavioratthetasklevel.Atthesametime,themodelbehaviorislearnedbasedontheL*methodtorealizecompositionalverificationtoalleviatethestateexplosionproblem,andthecomposabilityoftherefinedmodelisverified.Finally,therefinementandverificationmethodsareevaluatedbysimulationexperimentsandthemaster-slaveintelligentvehicleexample.Therelevantdatashowsthat,therefinedmethodandcompositionalverificationmethodshavesomeperformanceadvantagesinprocessingtimeandmemoryconsumption.Keywordscyberphysicalsystem(CPS)；clockconstraintspecificationlanguage(CCSL)；composiabilityofcomponent；L*algorithm；refinementoftimingbehavior摘要信息物理系统（cyberphysicalsystems,CPS）通常被应用于安全关键的场景中，需要进行实时监控，并计算反馈...
