操作语义

作品数：92被引量：135H指数：6
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：钱俊彦何炎祥赵岭忠古天龙宋国新更多>>
相关机构：上海交通大学华东师范大学武汉大学华东理工大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划广西壮族自治区自然科学基金国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
舰载机弹药保障作业调度的形式化建模与验证
《软件学报》2024年第9期4100-4122,共23页金钊 金璐 张博闻 吴庆顺 冯朔 李冠峰 徐明亮 
国家自然科学基金(62325602,62302459,62036010,61972362,62372416)。
航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证...
关键词：舰载机弹药保障作业 形式化验证 分离逻辑 操作语义 COQ 
基于函数式语义的循环和递归程序结构通用证明技术
《软件学报》2023年第8期3686-3707,共22页李希萌 王国辉 张倩颖 施智平 关永 
国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)。
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明...
关键词：程序验证 大步操作语义 定理证明 Coq定理证明器 
用OwlReady2实现智能人机对话系统
《电脑编程技巧与维护》2020年第7期116-119,共4页宋丛威 
为了对话机器人更加智能,用OwlReady2实现具有逻辑推理能力的人机对话系统。OwlReady2是本体论知识管理的描述语言OWL的Python接口,封装了推理引擎HermiT和Pellet,可以进行基于描述逻辑(DLs)的推理。对作为陈述句和疑问句的DLs表达式给...
关键词：OwlReady2接口 描述逻辑 推理引擎 人机对话系统 操作语义 
GSOS算子下共变-异变模拟的公理刻画被引量：1
《计算机科学》2020年第1期51-58,共8页李苏婷 张严 
国家自然科学基金(61602249);江苏省普通高校自然科学研究资助项目(17KJB520012)~~
进程的行为理论是进程演算研究的核心内容之一,其侧重于讨论进程间的行为等价和模拟关系。共变-异变模拟(Covariant-Contravariant Simulation,CC-模拟)的概念是对经典(互)模拟概念的推广,它通过区分动作类型,刻画了规范与实现对系统主...
关键词：GSOS 结构化操作语义(SOS) 进程演算 共变-异变模拟 可靠性 完备性 
ntyft/ntyxt算子下共变-异变模拟的前同余性
《计算机技术与发展》2019年第9期40-44,134,共6页李苏婷 张严 
国家自然科学基金(61602249);江苏省普通高校自然科学研究资助项目(17KJB520012)
进程代数是刻画并发与交互式反应系统行为的重要模型之一,进程间的(互)模拟关系及其公理化以及结构化操作语义(structural operational semantics,SOS)理论是其重要的两个研究方向。共变-异变模拟(covariant-contravariant simulation,...
关键词：结构化操作语义 共变-异变模拟 ntyft/ntyxt CC-ntyft/ntyxt 前同余性 分层 归约 
操作语义进行创造的心理模式
《集宁师范学院学报》2019年第3期99-103,共5页王义明 
创造可分为艺术创作、语言创造、科学发现、技术发明等类型。操作语义进行创造的心理模式主要为:打破定势;变换参照结构;重构;从语义交集再出发;变换视角;建构异常关联;对成品进行添加;合成;将部分从整体中分离;产生像似的语言;隐喻思维...
关键词：语义 创造 心理模式 认知 思维心理学 
Tabular表达式中正规函数表操作的形式语义
《华南理工大学学报（自然科学版）》2019年第2期85-91,共7页周文博 刘磊 张鹏 吕帅 
国家自然科学基金资助项目(61300049);中国博士后科学基金资助项目(2016M591482);吉林省自然科学基金资助项目(20150101054JC;20180101053JC;20190201193JC);吉林大学研究生创新基金资助项目(101832018C025)~~
正规函数表是一类典型的Tabular表达式,被广泛应用于软件说明文档.文中对Tabular表达式中正规函数表操作的语义进行研究.首先给出了正规函数表的形式文法,讨论了规整性、完全性和不可交叉性等性质,说明了其求值过程;然后根据操作的影响...
关键词：正规函数表 Tabular表达式 操作语义 软件文档 规格说明 
一种适用于可信编译器的源语言转换与检查框架被引量：1
《中国科技论文》2017年第14期1646-1650,共5页张晓曈 何炎祥 
国家自然科学基金资助项目(91118003;61373039);高等学校博士学科点专项科研基金资助项目(20130141110025)
针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换...
关键词：编译验证 可信编译器 代码转换 操作语义 
UML顺序图形式化语义的研究综述被引量：6
《计算机科学》2017年第2期17-30,64,共15页郭艳燕 张楠 童向荣 
国家自然科学基金项目(61403329;61502410;61572418);山东省自然科学基金项目(ZR2015PF010;ZR2013FQ020;ZR2014FL009;ZR2014FQ016);山东省高等学校科技计划项目(J15LN09;J14LN23)资助
为UML顺序图构建形式化语义,不仅有利于精确描述软件系统的动态交互过程,而且有利于进行基于UML模型的分析和验证,是有效提高软件系统可靠性的重要保障。结合近年来国内外对UML顺序图形式化语义的研究工作,分类阐述了各种方法,综合分析...
关键词：统一建模语言UML 形式化方法 顺序图 组合交互片段 指称语义 操作语义 
_mJava到Micro-Dalvik虚拟机的编译验证被引量：3
《电子学报》2016年第7期1619-1629,共11页江南 何炎祥 张晓瞳 
国家自然科学基金(No.61373039)
针对类Java的面向对象语言mJava到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证,给出了mJava语言和Micro-Dalvik的操作语义.从mJava语言程序到Micro-Dalvik虚拟机指令的编译分为两步,首先将mJava语言程序中的本地变量名转换为相...
关键词：编译验证 定理证明 操作语义 机器检测 寄存器架构 面向对象语言 
全选清除导出
共10页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部