论文部分内容阅读
使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之间的转移关系。基于这些性质,引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述。此外,在证明过程中,发现该程序中存在着一个很难通过现场测试发现的问题。
COQ定理证明器辅助PLC程序验证和分析
【摘 要】
：
使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之间的转移关系。基于这些性质,引入了逻辑自
【机 构】
：
LingcoreLaboratory,DepartmentofECE,清华大学软件学院
【出 处】
：
北京大学学报：自然科学版
【发表日期】
：
2010年01期
【基金项目】
：
国家自然科学基金资助项目（90718039）,致谢同Hugh Jack关于PLC语义问题的讨论使本文作者加深了对有关问题的理解.感谢评审人认真审阅并提出多项宝贵意见.
其他文献
台湾海峡及其邻近海区真囊水母属经研究有5个新种:顶室真囊水母(Euphysora apiciloculifera sp.nov.)、粗管真囊水母(Euphysora crassocanalis sp.nov.)、间腺真囊水母(Euphy
目的探讨增龄、性别对老年高血压患者血压昼夜节律及24 h动态脉压（24 h APP）的影响。方法将2014年7月—2015年6月住院的346例老年高血压患者按年龄段分为老年1组（60～69岁,n=77）、
本文应用准地转正压无辐散模式对双涡的相互作用进行了数值模拟试验.试验结果表明:(1)只考虑相对涡度平流的情况下双涡以互旋为主,而且随着初始间距的缩小,互旋越来越明显.(2
从南极普利兹湾深海900m的沉积物中筛选到一株同时产多种低温复合酶的菌株BH197,作者对其进行碳源、氮源、无机盐、起始pH值、培养时间、接种量等发酵条件的优化实验.实验结
本文初步建立了直接测定海水中溶解色氨酸的方法,并进行各种条件影响实验.在0～0.070 mg/dm3浓度范围内色氨酸荧光强度与浓度之间线性关系良好.在最佳实验条件下,方法检测限为7