论文部分内容阅读
信息物理系统(Cyber Physical Systems,CPS)的功能及其复杂程度在与日递增的同时需要满足严苛的安全性要求,使得在系统开发过程中需求层至实现层必须进行时间行为正确性、安全性的分析与验证。时钟约束描述语言(Clock Constraint Specification Language,CCSL)作为统一建模语言 UML2.0 的扩展附件已被业界广泛关注,其定义了具有丰富语义的时间建模元素用于刻画CPS的时间行为,为组件的时间行为建模提供有效支撑。当前基于CCSL建模语言的时间行为分析与验证已经取得一些卓有成效的研究成果,然而依托CCSL语言进行CPS的开发与设计仍然缺少更为具体的组件时间行为组合操作方法、组件时间行为可组合验证规则等实现技术,类似问题仍是业界所面临的主要挑战。针对上述问题和技术需求,本文提出一种以CCSL语言为核心,基于时间行为模型的信息物理系统开发框架。在该框架中,利用逻辑时钟及时钟间关系建立系统的时间行为模型,并在此基础上给出组件时间行为组合操作方法,组件时间行为可组合的形式化定义等具体实现技术。基于此,本文具体工作内容及贡献如下:(1)提出一种基于时钟迁移系统的组件时间行为组合操作方法。借鉴CCSL中逻辑时钟的概念建立组件时间行为模型,将逻辑时钟的滴答行为建模为迁移系统中的迁移动作以简化复杂的中间形式化语义转换,并进一步给出基于时钟迁移系统的组件时间行为组合操作方法。同时给出基于乐观组合思想的时间行为可组合的形式化定义,为组件的时间行为分析与可组合验证奠定理论基础。(2)针对时间行为模型在组合后产生的状态爆炸问题,提出一种基于L*学习的启发式分组组合验证框架。框架基于分治思想将对整体模型的属性验证转换为对个体模型应具有行为属性的过程推导,以此缓解时间行为模型在组合后由于状态爆炸导致验证难的问题。同时考虑到任务时间行为的差异性,将行为的学习过程划分为无时间行为属性推理与有时间行为属性推理两个阶段,并给出启发式的分组验证策略以进一步划分组件来减少模型验证次数从而提高验证效率。实验结果表明,采用启发式分组的验证方法相较未采用分组的验证方法所用时间缩短18.66%至36.67%,内存消耗上降低32.43%至47.99%。在时间行为的验证性能方面,与现有采用时间自动机语义的UPPAAL工具方法相比较,验证所用时间缩短37.15%至48.12%。实验过程可见,对于某些因内存消耗较大导致无法完成验证的场景,采用启发式分组的组合验证方法也均可得到相应的验证结果。(3)给出从需求模型到任务模型的时间行为精化方法。考虑到安全关键CPS的场景特征,方法对延迟约束、关联约束及输出间隔约束三种时间行为进行具体精化,更加契合CPS的功能需求层对于时间约束行为的表达要求。给出任务图结构建立上层时间行为需求模型与下层具体任务时间行为模型之间的关联,最终生成任务的周期、相位与截止时间等属性值。精化方法引入资源利用率对任务执行周期的取值范围进行限定,进一步缩小任务集的解空间并有效降低解空间的迭代搜索次数,同时使得所生成的任务集在保证任务可调度的前提下具有最优的执行性能。随机选择区间为0~1000的组件数量进行任务集生成的仿真测试,多次实验结果显示,在精化方法的可扩展性上,时间行为精化方法相较UML-RT精化方法平均减少0.11次迭代搜索次数(取自然对数),相较通过分解-合成的Shige精化方法平均减少3.16次迭代搜索次数。在精化方法的有效性上,本文所给精化方法通过利用率对所生成的任务集进行限定,在满足系统时间约束关系的前提下,生成任务集的资源利用率较改进前可提升15.22%。(4)以主从智能小车系统作为实际案例进行开发实践。首先采用CCSL语言建立组件的时间行为需求模型,并通过精化方法得到具体任务的时间属性值。对应智能小车功能版本CAR-1,2,3,分别定义32、41和49个逻辑时钟用于描述任务释放、抢占、结束等行为,以此构建整体任务的时间行为模型。其中在给出WiFi网络时间行为模型的基础上进一步抽象WiFi组件的不同工作状态,形成了一种新颖的WiFi网络传输行为分析及功耗预测方法,实验数据表明功耗预测值与真实值相对误差有效的在7.12%范围内。最后分别对小车系统的正确性、可组合性等功能/非功能属性进行验证,相关统计数据也表明本文所给精化方法和组合验证方法的性能在一定程度上优于改进前的方案。综上所述,本文对信息物理系统中组件的时间行为建模及分析进行了理论与方法上的研究。具体工作包括,提出了时间行为模型的组合操作方法,给出时间行为可组合的形式化定义,提出了基于L*学习的组合验证方法,以及时间行为模型的精化方法,并在此基础上对主从智能小车系统进行了具体开发与分析。相关实验及统计数据表明,本文研究具有一定的理论意义和工程实践价值,对信息物理系统的开发与设计也起到了积极的促进作用。