【摘 要】
：
对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在,而是关心状态组合提供的功能是否存在及各状态
【机 构】
：
北京交通大学电子信息工程学院,北京交通大学电子信息工程学院 北京100044,北京100044
论文部分内容阅读
对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在,而是关心状态组合提供的功能是否存在及各状态组合之间是否存在指定的转换关系,从而避免了状态空间爆炸问题。模块搜索算法以模块为基础对任务流模型进行搜索来验证给定系统是否满足规范要求。
The task flow model checking technique is discussed. The task flow method does not care about the number of states, whether it can reach another specified state from one specified state or not, and whether the function provided by the state combination exists and whether there is a specified conversion relationship between the state combinations, Thus avoiding the state space explosion problem. The module search algorithm searches the task flow model on a module-by-module basis to verify that the given system meets the specification requirements.
其他文献
摘要：本文通过对电子行业制造商特点的分析，提出了一套适用于该行业的供应商评 价指标体系。同时将层次分析法和灰色关联理论相结合，提出了一种新的供应商评价方法。通过实例分析，说明该方法直观可靠，是一个可行的供应商评价方法。 关键词：电子制造；供应商；层次分析法；灰色关联度分析 中图分类号：TP311文献标识码：A 文章编号：1009-3044(2007)03-10776-01 1 引言
实时性是嵌入式应用中一个重要的指标,而优先级翻转是影响系统实时性的一个重要因素.可剥夺型内核中,任务以独占方式使用共享资源时,将出现低优先级任务先于高优先级任务运行
植物措施是水土流失防治措施的重要组成部分,它具有投入少、见效快、生态效益好等优点,越来越被人们重视与采纳.鸟山矿井及选煤厂水土保持植物防护措施是针对不同的防治分区,
摘要：机器翻译是对人工翻译的模拟。但是由于不同语言之间历史文化、风俗习惯等因素存在固有差异，所以相同的文字时常在不同环境下表达的意义不同，这使得机器翻译实现十分困难。 独词句是语言学上的一种特殊的句型。独词句需要根据上下文环境来判断它的“句义”，而不仅仅是它的“词义”。然而目前大多数的计算机翻译软件，对独词句的处理都存在缺陷。本文希望能从语言学的角度，对翻译系统处理独词句提出更为合理的解决方法。
摘要：步进电机控制实验是微机原理与接口技术课程中一个非常重要的实验。研究了步进电机控制实验存在的问题，提出了改进实验内容，提高实验效果的措施，充分发挥了实验系统所提供的资源，有效地促进了实验效果地提高。 关键词：步进电机；控制；微机接口 中图分类号：TP331 文献标识码：A文章编号：1009-3044(2007)03-10790-01 1 引言 步进电动机是一种把电脉冲转换成角位