具有程序的静态结构和动态行为语义的时序逻辑

来源 :计算机研究与发展 | 被引量 : 0次 | 上传用户:saoluan
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
提出一种区间分支时序逻辑——控制流区间时序逻辑(control flow interval temporal logic,CFITL),用于规约程序的时序属性.不同于计算树逻辑(computation tree logic,CTL)和线性时序逻辑(linear temporal logic,LTL)等传统的时序逻辑,CFITL公式的语义模型不是基于状态的类Kripke结构,而是以程序的抽象模型控制流图(control flow graph,CFG)为基础所构建的含序CFG结构.含序CFG是CFG的一种受限
其他文献
“道法自然”是道家价值理念的核心,对高校大学生伦理意识的构建与提升具有积极的借鉴意义。要让大学生对伦理意识的构建情由心生,达到“愿学了、真懂了、全信了、会用了”的四
文章主要介绍了目前各种主流EOC技术及其特点,选择原则,以及广电网络适用的EOC技术。
在电子政务外网中设计网络设备远程管理系统,将全网各级机房的所有网络串口设备进行集中控制和管理。该系统包括集中认证审计管理、多种网络接入方式远程管理和设备管理三部分
随着集成电路技术的迅速发展,芯片的集成度不断提高,片上众多处理单元间的高效互连成为关键问题,因而相继出现了片上系统(system-on-chip,SoC)和二维片上网络(two-dimensional n
提出了一种软硬件协同的物联网可重塑终端架构EasiSHA,采用以可重塑计算部件为核心的终端体系结构,能够针对应用需求动态调整软硬件资源配置,在提供较高通用性的同时能够有效降低终端的硬件冗余度.提出了一种软硬件任务调度机制,根据物联网应用运行时所需终端的性能指标,实时动态改变计算任务的执行方式,在终端性能满足应用需求的前提下优化终端整体功耗.提出了一种计算任务复用机制,采用软硬件协同的方式实现应用程
当前信息安全形势下,大部分高校开设了网络安全课程,其中渗透测试技术的学习举足轻重。文章分析了各类常用的渗透测试工具,并着重对Web Goat这一开源的渗透测试平台进行研究