首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  免费   0篇
  国内免费   3篇
自动化技术   3篇
  2018年   1篇
  2015年   2篇
排序方式: 共有3条查询结果,搜索用时 15 毫秒
1
1.
中断驱动系统模型检验   总被引:1,自引:1,他引:0  
针对一类中断驱动系统提出了一种建模和模型检验的方法.该系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理.因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效.为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高系统的正确性,首先确定了此类系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数.然后,提出了将这些要素和参数自动转化为形式化模型的方法:使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模.对于得到的形式化模型,给出了针对中断处理超时错误的检测方法,并在此基础上给出了针对共享资源的完整性、子程序原子性的检验方法.  相似文献   
2.
周筱羽  顾斌  赵建华  杨孟飞 《软件学报》2015,26(10):2485-2503
针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.  相似文献   
3.
云计算和移动互联网的不断融合,促进了移动云计算的产生与发展.在移动云计算环境下,用户可将工作流的任务迁移到云端执行,这样不但能够提升移动设备的计算能力,而且可以减少电池能源消耗.但是不合理的任务迁移会引起大量的数据传输,这不仅损害工作流的服务质量,而且会增加移动设备的能耗.基于此,本文提出了基于延时传输机制的多目标工作流调度算法MOWS-DTM.该算法基于遗传算法,结合工作流的调度过程,在编码策略中考虑了工作流任务的调度位置和执行排序.由于用户在不断移动的过程中,移动设备的无线网络信号也在不断变化.当传输一定大小的数据时,网络信号越强则需要的时间越少,从而移动设备的能耗也越少.而且工作流结构中存在许多非关键任务,延长非关键任务的执行时间并不会对工作流的完工时间造成影响.因此,本文在工作流调度过程中融入了延时传输机制DTM,该机制能够同时有效地优化移动设备的能耗和工作流的完工时间.仿真结果表明,相比MOHEFT算法和RANDOM算法,MOWS-DTM算法在多目标性能上更优.  相似文献   
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号