期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到77篇文章
< 1 2 … 4 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
Agent组织结构设计的一种形式语义 被引量：13
1
作者 张伟 石纯一 《软件学报》 EI CSCD 北大核心 2002年第3期447-452,共6页
Agent组织是多Agent系统研究的重要方面,在不同的Agent组织形成方法中常采用显式的组织形成方法.基于p演算和化学抽象机给出了组织结构设计过程的一种形式语义.把参与组织结构设计的有关Agent都作为化学抽象机中的化学分子,而化学抽象... Agent组织是多Agent系统研究的重要方面,在不同的Agent组织形成方法中常采用显式的组织形成方法.基于p演算和化学抽象机给出了组织结构设计过程的一种形式语义.把参与组织结构设计的有关Agent都作为化学抽象机中的化学分子,而化学抽象机的运行过程即是组织结构的设计过程.这种语义给出方式准确、直观,使组织结构设计系统易于实现,改进了Ferber和Xu关于Agent组织的操作语义和组织结构设计的工作. 展开更多
关键词 MAS AGENT 组织结构 形式语义 Π演算 抽象机 人工智能
下载PDF
形式化方法B及其程序规约机理 被引量：16
2
作者 肖美华 薛锦云 《计算机工程》 CAS CSCD 北大核心 2004年第16期16-18,50,共4页
用形式化方法开发软件是提高软件可靠性和生产效率的革命性途径,是实现软件自动化的关键。文章针对B方法,介绍了其产生的历史背景,分析了其程序规约机理,并结合实例给出了B方法中抽象机的具体运用,对该方法的特点进行了评述。
关键词 形式化方法B 程序规约 抽象机 程序设计
下载PDF
形式化方法B的证明技术 被引量：4
3
作者 鹿蕾 《现代电子技术》 2005年第23期126-128,共3页
用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动化的关键。形式化方法B是借助于其辅助工具支持从规约到实现的全过程开发工作。本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查... 用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动化的关键。形式化方法B是借助于其辅助工具支持从规约到实现的全过程开发工作。本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性。 展开更多
关键词 形式化方法 抽象机 广义代换 类型检查 证明义务
下载PDF
形式化方法B的精化
4
作者 高洪江 覃征 +1 位作者 鹿蕾 邵利平 《计算机工程》 CAS CSCD 北大核心 2007年第9期49-51,共3页
形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理... 形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化。 展开更多
关键词 形式化方法 广义代换 抽象机 前向精化 反向精化 证明义务
下载PDF
基于B方法的弹道计算机程序设计技术 被引量：2
5
作者 张子丘 郑宇军 李海英 《计算机工程与设计》 CSCD 北大核心 2005年第12期3295-3297,3300,共4页
针对任务关键性的武器装备控制领域,选用B方法来设计通用弹道计算机程序,显著地提高了软件的质量和可靠性。在开发过程中,利用抽象机机制对基本弹道计算机进行建模,并通过逐步精化的方法扩展弹道计算机功能,从而有效地控制了弹道计算参... 针对任务关键性的武器装备控制领域,选用B方法来设计通用弹道计算机程序,显著地提高了软件的质量和可靠性。在开发过程中,利用抽象机机制对基本弹道计算机进行建模,并通过逐步精化的方法扩展弹道计算机功能,从而有效地控制了弹道计算参数之间的复杂关系,依赖不变式技术形式化地保证了软件运行时的安全性,并使得生成的程序具有良好的重用性和可扩展性。 展开更多
关键词 B方法 形式化方法 弹道计算机 抽象机 不变式
下载PDF
基于Web的网络旅游服务系统的形式化B开发 被引量：1
6
作者 李信本 《计算机工程》 CAS CSCD 北大核心 2007年第7期282-284,F0003,共4页
形式化B方法支持从规格说明到代码生成的全部软件开发过程。结合网络旅游服务系统模型,讨论了形式化B方法的具体运用,在分析服务器端和客户端状态表示的基础上,给出了该系统的抽象机模型及其精化过程。
关键词 形式化方法 B方法 WEB技术 抽象机
下载PDF
一个抽象机库中B方法的研究 被引量：1
7
作者 杨丹 梁洪峻 《微计算机应用》 2007年第10期1117-1120,共4页
B方法是支持规格说明到软件设计和执行的形式化方法。文章研究了B方法中一种抽象机库的实现模型和生成代码,对该方法的特点进行评述。验证了B的正确可靠的实现方法,充分利用B方法的精化原则,提高了B形式化方法的开发验证效率。
关键词 B方法 抽象机 精化 证明义务
下载PDF
UML模型到B抽象机的转换和实现 被引量：1
8
作者 仲晓敏 邹盛荣 《计算机时代》 2007年第11期44-46,共3页
统一建模语言UML广泛用于面向对象技术的建模,B方法主要是用抽象机来描述软件系统的规格说明。文章针对软件开发中经常用到的UML模型,提出了基于B语言的UML形式化方法:通过将UML模型转化为B抽象机,实现了UML模型的形式化。实例分析表明... 统一建模语言UML广泛用于面向对象技术的建模,B方法主要是用抽象机来描述软件系统的规格说明。文章针对软件开发中经常用到的UML模型,提出了基于B语言的UML形式化方法:通过将UML模型转化为B抽象机,实现了UML模型的形式化。实例分析表明,转换是可行的。 展开更多
关键词 UML 形式化方法 抽象机 B方法
下载PDF
B方法在家庭智能控制系统开发中的应用
9
作者 王友 张广泉 《计算机工程与应用》 CSCD 北大核心 2006年第24期80-83,共4页
精确的软件需求规约是确保软件质量的基础,软件过程中保证方法更为重要,良好的方法可以保证在产品的开发过程中不引入人为的错误。现有流行的软件过程方法都可以在一定程度上减少此类错误的引入,很难从本质上避免人为错误的引入,形式化... 精确的软件需求规约是确保软件质量的基础,软件过程中保证方法更为重要,良好的方法可以保证在产品的开发过程中不引入人为的错误。现有流行的软件过程方法都可以在一定程度上减少此类错误的引入,很难从本质上避免人为错误的引入,形式化方法以其精确的数学语义为基础,可以保证开发过程中的一致性和准确性,以B方法尤为突出,它可以适用于软件过程中的任一阶段。文章以家庭智能控制系统为例,介绍了B方法在软件开发过程中的应用。 展开更多
关键词 B方法 软件过程 抽象机 形式规约 软件设计
下载PDF
UML与B结合的软件开发研究与应用 被引量：2
10
作者 廖青松 马光思 《计算机技术与发展》 2007年第6期123-126,154,共5页
B方法主要是用抽象机来描述软件系统的规范说明,且有大量工具支持。UML已广泛用于面向对象技术的建模,许多工程项目和研究成果用UML图例给出。文中将B方法与UML结合用于软件的开发过程,结合工程实际和文献资料分析了从UML的类图、时序... B方法主要是用抽象机来描述软件系统的规范说明,且有大量工具支持。UML已广泛用于面向对象技术的建模,许多工程项目和研究成果用UML图例给出。文中将B方法与UML结合用于软件的开发过程,结合工程实际和文献资料分析了从UML的类图、时序图和状态图转换到B的抽象机的技术要点,通过实例展示了具体的转换形式。 展开更多
关键词 B方法 UML 软件规格说明 抽象机
下载PDF
B方法规格说明的构造及应用 被引量：1
11
作者 吴帅 杨庆红 樊艳芬 《计算机与现代化》 2007年第5期29-32,35,共5页
B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期。本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行... B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期。本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行了一次精化。 展开更多
关键词 规格说明 B方法 抽象机 证明义务 精化
下载PDF
基于操作语义的时间隐通道分析 被引量：1
12
作者 戴梅 孙国强 刘志锋 《计算机工程与设计》 CSCD 北大核心 2009年第7期1593-1595,1599,共4页
主要讨论了计算机信息安全领域中比较热点的话题——基于操作语义的时间隐通道。根据隐通道中的时间隐通道的特点和存在的最小条件,针对其特点提出了一种搜索方法。该搜索方法将进程看作一个抽象机状态机,以Plotkin的结构化操作语义等... 主要讨论了计算机信息安全领域中比较热点的话题——基于操作语义的时间隐通道。根据隐通道中的时间隐通道的特点和存在的最小条件,针对其特点提出了一种搜索方法。该搜索方法将进程看作一个抽象机状态机,以Plotkin的结构化操作语义等推导规则为基础,以及完整的信息传导操作语义的模型,分析了两个高低安全级进程抽象机状态变化及其状态动态变化序列,最后对可视窗口的分析,可以找到其中存在的时间隐通道。 展开更多
关键词 隐通道 时间隐通道 抽象机 信息传导 结构化操作语义
下载PDF
应用基于抽象机的动态翻译设计Java处理器 被引量：1
13
作者 王海晨 赵祥模 《微电子学与计算机》 CSCD 北大核心 2012年第7期1-3,7,共4页
本文提出了一种基于硬件抽象机的动态翻译技术,它可用于实现Java处理器.该技术采用了硬件抽象机的"模糊执行"(HAM)方法,通过分析Java程序之间的相关性,动态地将Java字节码转换成基于标签的类RISC指令.然后,将堆栈折叠与动态... 本文提出了一种基于硬件抽象机的动态翻译技术,它可用于实现Java处理器.该技术采用了硬件抽象机的"模糊执行"(HAM)方法,通过分析Java程序之间的相关性,动态地将Java字节码转换成基于标签的类RISC指令.然后,将堆栈折叠与动态翻译相结合进一步优化指令.应用该技术设计了一个Java指令级并行处理器,并且扩展它,支持Java多线程功能. 展开更多
关键词 二进制翻译 抽象机 JAVA处理器 多线程
下载PDF
一种自动机学习和符号化执行的软件自动测试方法 被引量：1
14
作者 陈曙 叶俊民 张帆 《计算机科学》 CSCD 北大核心 2013年第8期161-164,共4页
针对高可信软件提出一种软件脆弱性自动测试方法。与传统测试方法不同,该方法对待测试程序进行预处理,使用自动机学习算法构造软件与环境交互的抽象机模型,在符号化执行迭代过程中利用抽象机模型指导符号化执行,并动态生成测试数据,同... 针对高可信软件提出一种软件脆弱性自动测试方法。与传统测试方法不同,该方法对待测试程序进行预处理,使用自动机学习算法构造软件与环境交互的抽象机模型,在符号化执行迭代过程中利用抽象机模型指导符号化执行,并动态生成测试数据,同时精化交互抽象机用于后继的符号化迭代测试。解决了传统符号化执行测试技术中缺乏指引、具有较高盲目性的问题,同时也提高了符号化执行测试的效率和代码覆盖率。 展开更多
关键词 自动机 自动测试 符号化执行 抽象机
下载PDF
基于Warren抽象机的Prolog实现技术的研究 被引量：1
15
作者 张晨曦 慈云桂 《计算机学报》 EI CSCD 北大核心 1990年第10期756-762,共7页
本文介绍了基于WAM的Prolog实现技术的研究结果。首先论述了新的Prolog执行模型WAM-PLUS。该模型由扩充了的WAM和非逻辑成分执行机制NLEM构成。它能支持Prolog动态代码,并能实现一致的动态代码语义。文中还介绍了Prolog编译策略和Prolo... 本文介绍了基于WAM的Prolog实现技术的研究结果。首先论述了新的Prolog执行模型WAM-PLUS。该模型由扩充了的WAM和非逻辑成分执行机制NLEM构成。它能支持Prolog动态代码,并能实现一致的动态代码语义。文中还介绍了Prolog编译策略和Prolog编译器的设计,描述了一种顺序推理机的系统结构。 展开更多
关键词 抽象机 PROLOG
下载PDF
抽象机模式 被引量：1
16
作者 JuIio Garcia-Marin Miguel Sutil-Marin 马维达 《Internet信息世界》 2003年第1期87-91,共5页
由于现代高级编程语言和现有硬件之间的差异日渐增大,常常有必要引入中间语言、并在原始硬件之上构建抽象机。本论文描述了抽象机(Abstract Machine),一种对抽象机的本质特性进行捕捉的结构型模式;这些特性给出了对抽象机的定义。该模... 由于现代高级编程语言和现有硬件之间的差异日渐增大,常常有必要引入中间语言、并在原始硬件之上构建抽象机。本论文描述了抽象机(Abstract Machine),一种对抽象机的本质特性进行捕捉的结构型模式;这些特性给出了对抽象机的定义。该模式将抽象机的静态特性和动态特性作为分离的组件进行描述,并且还考虑了指令集和这些指令的语义,以及此模式的其他一些重要组件。 展开更多
关键词 抽象机 虚拟机 设计模式 程序语言
下载PDF
从ESTELLE协议规格说明生成测试序列
17
作者 蔡云飞 《工程兵工程学院学报》 EI 1992年第1期63-69,共7页
ESTELLE是一种由ISO提出的用于描述计算机通信协议的形式化描述技术,并已成为国际标准。随着计算机网络技术的发展,出现了一门新的学科——协议工程。它包括通信协议的规范、验证、生成、测试。测试序列生成在协议一致性测试中是一个非... ESTELLE是一种由ISO提出的用于描述计算机通信协议的形式化描述技术,并已成为国际标准。随着计算机网络技术的发展,出现了一门新的学科——协议工程。它包括通信协议的规范、验证、生成、测试。测试序列生成在协议一致性测试中是一个非常复杂的问题。本文提出了从ESTELLE语言规范生成测试序列的方法。有关测试序列生成的一些原始材料可以在一些协议规范的文本中找到。_抽象机(即扩充的有限自动机)是所提方法的基础。这个方法的思想是这样的:首先是用ESTELLE语言编译器从ESTELLE协议文本中提取要求的信息(抽象机),并且用某种形式表尔之。第二,将抽象机展开成为一个一般的有限自动机。第三,从有限自动机中生成测试序列。最后,把测试序列转换成TTCN形式。 展开更多
关键词 协议规格说明 抽象机 测试序列
下载PDF
基于CHAM的软件连接件形式化模型
18
作者 张淑娟 《信息与电脑（理论版）》 2013年第9期82-83,共2页
软件技术目前来看是日新月异,各种手段方法纷纷而至,但是随之到来的是其中存在的问题,大小问题比比皆是,下面就针对这一问题展开讨论,讨论的内容包括对化学抽象机CHAM的概述、基于CHAM的形式化模型的描述以及对存在的问题进行简要分析,... 软件技术目前来看是日新月异,各种手段方法纷纷而至,但是随之到来的是其中存在的问题,大小问题比比皆是,下面就针对这一问题展开讨论,讨论的内容包括对化学抽象机CHAM的概述、基于CHAM的形式化模型的描述以及对存在的问题进行简要分析,目的在于通过此次的讨论研究进一步地实现简化软件连接件的设计并且在此基础上提高软件连接件的通用性能。 展开更多
关键词 CHAM 形式化模型 软件体系结构 连接件 抽象机 构件系统 系统构件 集成测试 软件系统 测试覆盖
原文传递
一则双的声明 关于2010台北双年展Sputnik卫星计划
19
作者 黄建宏 陈泰松 《当代艺术与投资》 2010年第10期21-23,共3页
失去功能的卫星,在空中飘荡,不是因外力所致,而是来自它本身;我要停摆这个装置,2010年台北双年展内建的批判机制。这不是要离弃它,反而是要让它以这种失能示人;这是一种自我客体化,但不是为了自我批判,因为如今若不是流于虚矫,便是为了... 失去功能的卫星,在空中飘荡,不是因外力所致,而是来自它本身;我要停摆这个装置,2010年台北双年展内建的批判机制。这不是要离弃它,反而是要让它以这种失能示人;这是一种自我客体化,但不是为了自我批判,因为如今若不是流于虚矫,便是为了服众的修辞术。套用德勒兹说的"détraquées"(坏掉、出毛病)1,这只不过是要让这部机器——卫星——变得无法运转,行不通,让这部欲望机器故障,反批判机制的有机论。 展开更多
关键词 双年展 批判话语 卫星 德勒兹 台北 机制 抽象机 机器故障 欲望机器 当代艺术
原文传递
用于C交叉编译的HUST抽象机
20
作者 曹化工 韩宗芬 《华中理工大学学报》 CSCD 北大核心 1989年第2期25-30,共6页
HUST抽象机是专为面向多目标机的C交叉编译系统设计的一种抽象机。本文阐述了该抽象机的结构、特点及设计思想。与其他抽象机比,该抽象机执行速度快,具有查运行溢出错、越界访问数组元素错和类型转换溢出错的能力。
关键词 C语言 抽象机 编译系统 HUST
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 2 … 4 下一页 到第 页
使用帮助 返回顶部