【摘 要】
：
实时系统、嵌入式系统等反应式系统（Reactive Systems）往往具有“同步”特性,即模块间通信时间可忽略不计,同一时刻多个信号可同时发生.同步系统模型作为同步编程语言（如Esterel、Signal等）的基础,被广泛应用于反应式系统,特别是嵌入式系统的建模中.随着近年来物联网、信息物理系统等分布式实时嵌入式系统的蓬勃发展,同步系统的建模、规约与验证变得愈发重要.在同步系统中,基于“时钟约束
论文部分内容阅读
实时系统、嵌入式系统等反应式系统（Reactive Systems）往往具有“同步”特性,即模块间通信时间可忽略不计,同一时刻多个信号可同时发生.同步系统模型作为同步编程语言（如Esterel、Signal等）的基础,被广泛应用于反应式系统,特别是嵌入式系统的建模中.随着近年来物联网、信息物理系统等分布式实时嵌入式系统的蓬勃发展,同步系统的建模、规约与验证变得愈发重要.在同步系统中,基于“时钟约束”的系统规约在系统的安全性和可靠性方面扮演着关键角色.时钟约束规约语言（Clock Constraint Specification Language,简称CCSL）是一种基于“时钟”和时钟约束关系的形式化规约语言.它被广泛地应用于同步系统的规约与验证.以往CCSL规约的验证技术主要基于模型检测.由于模型检测技术的局限性,这些验证技术不支持无限状态CCSL规约（亦称为“非安全”CCSL规约）的验证.对于状态空间较大的系统,基于模型检测的验证技术存在状态空间爆炸的问题.动态逻辑（Dynamic Logic,简称DL）是一种对程序动态行为进行刻画和推理的模态逻辑,其验证技术主要基于定理证明和SMT检测.动态逻辑程序能（在抽象层）对系统行为进行建模,并配合动态逻辑公式对系统性质进行规约和验证.相较于基于模型检测的验证技术,基于定理证明的验证技术能够对无限状态系统进行验证,并从验证方法上避免了对状态空间的搜索.本文结合CCSL语言与动态逻辑DL,提出了一种基于时钟约束的动态逻辑（Clock-constraint-based Dynamic Logic,简称CDL）系统,将动态逻辑应用于同步系统的建模与验证中.CDL逻辑系统支持对同步系统建模,对基于时钟约束关系的同步系统CCSL规约进行刻画和验证;支持基于定理证明的“模块化”验证方法,能对“非安全”的CCSL规约进行验证.该系统为同步系统提供了一个基于定理证明技术的建模/验证框架.本文的主要贡献如下:1.提出了面向顺序程序的时钟约束动态逻辑（Sequential CDL,简称sCDL）,定义了其语法和语义,并构建了sCDL证明系统.sCDL逻辑系统在一阶动态逻辑（First-Order Dynamic Logic,简称FODL）系统的基础上,引入了“信号”和“CCSL时钟关系”并对其证明系统进行了扩展.sCDL逻辑系统支持对顺序同步系统行为进行建模,对顺序同步系统中一类“简单的”CCSL时钟约束关系进行刻画和验证.2.对sCDL逻辑进行“并行程序”的扩展,提出了时钟约束动态逻辑CDL,定义了其语法和语义,并构建了其证明系统.CDL逻辑在sCDL逻辑的基础上,引入了“并行算子”和“并行交互机制”,并对sCDL的证明系统进行了扩展.CDL逻辑实现了对（并行）同步系统行为进行建模,对基于时钟约束关系的同步系统CCSL规约进行刻画和验证.3.对CDL逻辑证明系统的可靠性和完备性进行分析,并证明了CDL逻辑证明系统的可靠性和相对完备性定理.4.通过两个同步系统案例——数字滤波器和车载自动窗系统,分析了CDL逻辑在同步系统中的应用.用CDL逻辑对同步系统进行了建模,描述并证明了它们的CCSL规约.结果表明了论文提出的方法是合理和有效的.
其他文献
已有的关于权力感与决策的相关研究,主要运用接近-抑制理论来解释相关结果,更多关注权力感高低维度对接近和抑制行为的影响,较少关注权力动机的高低及权力感的稳定性维度在其中所起的作用,且多数研究偏向于探讨收益情境下的接近行为,较少探讨损失情境下的抑制行为。特别是,关于权力感何以会影响和改变个体的接近和抑制行为,尚不清楚。本研究试图从风险偏好的视角入手,以实际工作中不同层级的领导干部群体为被试,采用收益损
加纳沃尔特河项目是20世纪60年代非洲一个具有重要影响的国际工程,其发展历程颇为漫长和复杂。自澳大利亚人艾伯特·凯特森在1915年提出沃尔特河项目构想后,吸引了很多私人公司的积极参与,其中又以南非工程师邓肯·罗斯领导下的西非铝业有限公司为首,同时也引起了英国及其黄金海岸殖民地政府的高度关注,他们推动着沃尔特河项目的早期发展。1953年,黄金海岸殖民地政府建立了以罗伯特·杰克逊为主席的沃尔特河项目筹
既有上博簡字跡研究已經取得了很好的成績,但在方法上,如何定量,以及如何合理選定用於字跡比較的典型字符等方面尚有進一步提升的空間,例如,列舉以下7個“典型字”論證《弟子問》與《君子為禮》2篇文獻的“文字書寫軌跡”具有同一性:“則、爲、者、遊、贛、而、富”。通過窮盡性調查,我們發現,“者、遊、富”《君子為禮》篇僅1見;“爲”《君子為禮》篇僅2見;“贛”《弟子問》篇僅2見,這些使用頻率較低的“典型字”,
可变剪接普遍存在于真核生物中,是基因表达调控的重要环节,通过外显子的不同组合可产生一系列差异转录本,在极大程度上丰富了生物体的转录组和蛋白质组多样性。同时,异常的可变剪接也将直接导致机体生理功能的紊乱。因此,可变剪接事件对于生物体正常生理功能的实现是至关重要的。唐氏综合征细胞黏附分子（Dscam）是可变剪接的代表性基因,在果蝇（D.melanogaster）中可潜在产生38,016种可变剪接异构体
本文综合新课程物理教材的胡克定律实验设计思想和创新的实验方法,对胡克定律的实验进行了改进,重点介绍了设计的弹簧弹力与形变量关系探究仪,该演示仪既可以精确地得出胡克定律,又可以对弹簧的劲度系数进行进一步的探究。
近几年来,同时基于光纤传输和星地传输的量子保密通信发展迅猛,世界主要国家高度关注量子信息技术发展,甚至上升为国家战略。早在2013年,我国就前瞻部署了世界首条远距离量子保密通信“京沪干线”,率先开展了相关技术的应用示范并取得系列宝贵经验。随着量子信息技术的不断发展,量子信息最常用的载体——通信波段红外光子的单光子探测技术也被推动向前。然而当前应用较广的近红外单光子探测器如InGaAs APD和SN
Ⅰ-Ⅱ-Ⅳ-Ⅵ族（其中Ⅰ=Cu或Ag;Ⅱ=Zn、Cd、Ni、Co、Fe或Mn;Ⅳ=Si、Ge或Sn;VⅠ=S、Se或Te等）多元化合物具有组成元素丰富、价格低廉、环境友好等优点以及优异的电学、光学、磁学和热学等物理性质,从而在太阳能光伏、热电、光催化、非线性光学等领域具有重要的潜在应用价值。该类材料的晶体结构通常遵循八隅体规则,其中阳离子具有相同的占位,随成分的变化可形成多种不同的有序结构。由于这
目的 分析切开根治术对低位肛周脓肿患者创面愈合速度、术后疼痛及肛门功能的影响。方法 选取本院2019年6月至2021年6月收治的106例低位肛周脓肿患者作为研究对象，根据治疗方案的差异分为研究组和对照组，各组53例。研究组患者接受切开根治术，对照组接受传统分期治疗（切开引流后行Ⅱ期肛瘘术）。对比两组创面愈合时间、术后首次排气时间和首次排便时间，比较两组术后肛门疼痛情况，以Starck评分和Wexn
移动分布式系统中的计算描述的是如何向分布在不同位置的用户提供高质量的信息服务,目前已经被广泛地应用于教育科研、国防军事、交通运输和航空航天等领域。移动计算的移动性和本身所处的环境会显著地影响通信质量,可能会导致原本可以通信的双方无法继续通信。因此如何刻画移动计算的特征和环境从而提高服务质量成为重要的研究点。本文使用形式化方法对移动分布式系统开展了研究,提出了移动分布式系统的进程演算BigrTiMo
量子点作为光电子器件的增益或吸收介质,其中一些关键科学问题尚待深入研究。量子点除了具有三维量子尺寸效应之外,其用于激光器和探测器等还可表现出低阈值电流密度、低噪声等特点,因而具有较高实用价值。采用阱中量子点的器件既可作为光探测器件,也可作为光存储器件（以下统称阱中量子点光电器件）,基于其较长的载流子寿命可以获得低暗电流、高探测率和波长可调等特点,但量子点光电探测器在信号读出方面仍存在一些需要解决的