【摘 要】
：
复杂实时系统的验证问题一直备受关注。验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大。观察者模式是一个额外的子系统,可以将复
【基金项目】
：
本文受四川省应用基础研究项目:嵌入式系统软件形式化验证技术研究(2014JY0112)资助.
论文部分内容阅读
复杂实时系统的验证问题一直备受关注。验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大。观察者模式是一个额外的子系统,可以将复杂的验证特性转换为简单的可达性问题,同时也可以避免使用复杂的验证算法。将Etienne和Nouha Abid等人提出的抽象的观察者模式应用到实时系统实例——Train-Gate系统中,采用UPPAAL工具对Train-Gate系统中的某些场景建立观察者模型,并采用对比实验将验证结果与无观察者模式状态下的验证结果进行对比。对比结果表明,使用观察者
其他文献
光电设备的检定一直存在自动化水平低、体积庞大、检测时间长等问题,为了提高检定效率,研制一套便携式光电设备自动检定系统十分必要.以某型光电设备的检定为例,详细介绍了系
工业组态软件的设计是复杂的,为了设计出灵活的、可扩展性好、易维护的工业组态软件,在采用面向对象的软件设计时,引入了设计模式的概念,这些模式来源于众多设计者多年的面向
在地面站设备中,对于遥感遥测、测控测角而言,伺服控制系统都是重要的组成部分;从一个实际运动地球卫星地面站的设计和改造角度出发,探讨了伺服控制系统的系统工作原理、系统构成、系统配置、技术分析、相应性能的标校和检测,详细的叙述了环路的传输函数的数学模型建立、设计以及建站时可采用的简易、实用的检验校准方法,并提出了在编写程序时应当注意的问题和方面,比较全面的阐述了地面站伺服控制系统的设计和改造的过程,并
信号调理是信号采集系统中重要的组成部分,课题通过对采样保持SCP模块(AMC3301)和专用SCP总线技术的研究,实现了高放大倍数及不同截止频率下信号的同步采集,该信号调理模块通
全自动上芯机是用于芯片生产后工序的关键设备之一,机器视觉伺服系统是提高该设备产能和质量的关键系统,而图像预处理和芯片定位是其机器视觉的关键技术之一。为了消除采集图像与真实图像之间的差异,实现芯片精确定位,采用中值滤波算法和直方图算法实现图像的去噪和增强,并分析了图像相似性测量算法实现快速模板匹配。实验结果证明了算法的有效性和可靠性,为进一步提高芯片缺陷检测的精度提供了保障.
分子筛氧浓缩器是机载分子筛制氧系统的核心部件,是飞机氧源系统的发展方向;但目前我国分子筛氧浓缩器保障还较为落后,急需研制先进可靠的分子筛氧浓缩器性能试验系统;提出基
针对数据中心间骨干网络中存在大量突发性强的小流而难以实时跟随流量变化对其进行带宽分配的问题,提出了基于Richards种群生长模型的数据中心骨干网络带宽分配策略（RBA）。该策
详细介绍了C&K度量方法,结合灰色关联分析的相关理论,提出了一种基于C&K度量方法和灰色关联分析的类设计质量评估方法。依据C&K度量阈值及可接受类的定义,可以推导出面向对象