一种基于Mealy!机的语义程序验证方法

语义验证是束缚语义软件和语义程序设计语言发展的问题之一,针对这一问题,在基于语义Web服务的语义程序设计语言SPL及其知识库业务领域本体(BDO)的基础上,提出了一种基于Mealy!机对SPL所编排的业务过程进行语义验证的方法,结合在线外汇交易平台的案例,详细描述了运用该方法进行语义验证的过程。通过案例证明,本方法有助于编写语义正确的语义程序。

一种面向语义Web服务的语义程序变换方法

语义程序变换是面向语义Web服务的软件设计方法的基础,语义程序只有通过程序变换后才能被运行环境执行和调用,然而目前还缺乏有效的语义程序变换方法。针对这一问题,基于语义编程语言SPL,提出了一种面向语义Web服务的语义程序变换方法。该方法通过对语义数据类型、语义规则、语义服务和语义流程等语义信息的有效变换,不仅提高了面向服务的程序设计的灵活性和健壮性,而且有助于提高业务流程的柔性和重用性。

基于符号表达式的程序语义缺陷警报关联识别方法

针对程序静态缺陷检测存在高误报需要耗费大量人力消除的问题,提出了一种程序语义缺陷警报关联的方法,通过挖掘警报间的深层次关联信息建立警报关联,有助于提升人工判定警报的效率。首先采用符号表达式与区间表示一个变量的取值,并基于符号表达式的逻辑关系建立了警报间的关联推导规则,然后在缺陷检测阶段根据缺陷触发条件识别出警报并推导出不同警报间的关联,最后根据警报间的关联关系对警报进行自动判定。通过对5个实际C工程的测试结果表明,本文所提方法可以有效识别出警报间的关联关系,能够有效减轻人工判定警报的工作。

基于轨迹的程序语义之一: 轨迹与语义对象

本文提出一种基于轨迹的指称语义框架，该框架结合了操作语义和代数语义的特征，避免使用专门的数学理论，将静态语义和动态语义结合在一起统一处理．本文及其续篇将通过一个中等规模的过程式模型语言来说明上述语义框架更适合描述真正的程序设计语言．本文首先引入轨迹概念和模型语言，然后讨论该语言的各句法成分所对应的语义论域。

XYZ/E面向对象程序语义概述

XYZ/E面向对象程序中表示对象概念的语言成分是代理机构:一种由一个数据包块和与之匹配的进程所组成的模块.在时序逻辑框架下给出了面向对象程序及其包含的各种语言成分的语义,并提供了几个用于证明这些语言成分之间的语义一致性的定理.

两维时间域上的实时程序语义

超稠密计算模型是实时系统的一种重要抽象模型．该文首先简要介绍一种两维的超稠密时间域及在该域上定义的一种区间逻辑，然后用一个并行模型语言（类Ｏｃｃａｍ 语言）讨论用这种逻辑定义并行语言（在超稠密模型中）的时间语义的问题。

基于程序语义的计算机病毒检测方法

通过分析病毒程序的典型传染行为模式,总结出传染模块的典型语义特征,形成描述其语义特征的语义关系框架,在此基础上提出了一种针对未知病毒的检测方法——基于程序语义的病毒检测方法。该方法是通过抽取程序的语义关系框架,将之与病毒的语义关系框架进行匹配,达到检测未知病毒的目的。模拟实验中选取三种病毒作为样本,检测了20个程序,结果表明,在阈值D=0.9时,检测的准确率为87.5%。

语义Web应用程序:性质与开发模型

语义Web应用程序是应用语义Web技术开发的Web应用程序,其特点是全部信息均由应用程序本体所定义的概念进行标记,因而含有丰富的语义,能更好地支持信息集成和知识共享,从而能够更加充分地利用已有Web资源。给出语义Web应用程序的定义、构成与性质;说明应用程序本体与知识库的作用;建立语义Web应用程序的开发模型。通过编写一个基于计算机文献本体的语义Web应用程序,用实例验证了所提出开发模型的可行性以及在信息集成和信息检索方面取得的明显效果。

人工智能难题和程序语义学

句法机如何成为语义机是人工智能面临的难题,也是当代意向性理论研究的重点。程序语义学是试图解释这一问题的重要致思取向。它认为传统的人工智能、计算机科学等是以模态理论语义分析为基础的,其研究尚停留在符号的层面,而未涉及到真值、指称,即没有涉及到语言与世界的关联。在揭示语言与世界关联如何实现的问题上,程序语义学强调语义不是由对指称的计算所给予的,也不是由谓词逻辑的标准语义学所给予的,而是由程序给予的。程序语义学不但能够融合如福吉勒特等意义理论的局限,而且所提出的过程性分析和知识对于人工智能的研究、发展亦有启示性。

语义Web应用程序开发方法及实例分析

随着语义Web技术的不断发展,语义Web应用程序越来越受到重视,但现在国内对语义Web应用程序的研究却比较少,缺少语义Web应用程序的开发方法。文中通过对语义Web应用程序的研究,结合与Web应用程序的对比分析,给出了语义Web应用程序的定义、架构以及开发方法,并详细说明了基于数据层、逻辑层和表现层三层架构的语义Web应用程序的结构特征和构建过程,进而通过构建一个语义Web应用程序实例对所提出的开发方法进行了验证,取得了预期的成果。

试论程序语义基础下计算机病毒的检测方法

程序语义是计算机技术中一项非常重要的内容,也是计算机程序的核心部分,而通过对程序语义进行检测可以有效的识别出系统中的病毒程序。因此,本文就程序语义基础下计算机病毒的检测方法展开研究和分析。

关于学生程序自动语义查错

本文旨在介绍一个自动语义查错交互式系统中所给出的变量定值作用域的划分算法和以循环结构为单位的语义诊断策略。使用所给出的算法和策略,在多数情况下,可以提高语义查错的准确性和语义查错的效率。

程序代码中隐含数据与控制的Petri网建模技术

应用一种Petri网扩展CNets,描述程序代码中所隐含着的数据与控制,分别给出了程序代码的数据视图和控制视图.在CNets规范的基础上,研究程序中的数据与控制流之间的交互以及程序中数据、操作和资源之间的关系,同时给出CNets规范向经典Petri网规范的转换规则.在不运行程序的前提下,根据这一映射机制,通过CNets规范,利用经典Petri网理论对程序的性质进行分析.

Verilog代数语义研究

给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互模拟的.研究了此代数语义的相对完备性,即参照前面的操作语义模型,相对于扩展Verilog语言的一个子集而言,此代数语义是完备的.即所有符合这样语法的程序,如果它们是互模拟等价的,那么它们同样可以在所提出的代数系统中被推导相等.在完备性证明过程中,采用范式方法,即构造一种语法上特殊的程序,任何属于上述子集中的一个程序通过该代数规则都能够被转化为范式程序,而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的.上述结果具有重要的理论意义,因为现有的进程代数理论主要是针对管道通信并行语言而展开的,而对于像Verilog这种以共享变量通信为基础的复杂并行语言研究还是比较少的,对此类复杂的基于共享变量的并行语言的进程代数理论研究提出了一种通用、有效的方法.

真稳定类与辩论语义

稳定类语义和辩论语义是逻辑程序语义学研究方面突出的两种语义统一框架理论，它们统一了一些很重要的语义．因为它们有着不同的直觉和概念，它们的相互关系并不清楚．我们在它们最基础的概念层次上证明了，常规逻辑程序句法下二者是等价的，它们有着同样的语义统一能力．基于这个结果，我们为有前途的辩论语义指明一种迭代构造的方法．

程序错误的形式化定义和程序容错能力的分级

针对程序失效相关概念的形式化定义和程序容错能力的分级,分析了程序缺陷、状态偏差以及程序失效等基本概念之间的差异,并在基于状态的程序行为理论的框架下,形式化定义了这些概念.从程序安全和活性的可满足性方面,给出了一个程序容错能力的分级方案,有助于相关概念的准确理解以及系统的对现有方法容错能力的区分.

基于Assume-Guarantee搜索复用的C程序验证方法

提出了一种基于Assume-Guarantee搜索复用的验证方法,对C程序源代码进行验证.其思想是,在程序的每点处都引入一个保守假设条件,并假设从任意点出发,变量取值满足该点假设条件的所有执行路径都不会违背给定性质,然后根据这些假设条件遍历所有可能的执行路径以验证给定的时序安全性质,并在遍历的过程中验证这些假设条件是否满足,如果不满足,则不断对其精化和加强.验证方法总是在保证假设条件可靠的前提下尽量使用较弱的条件,使得大量的执行路径由于满足假设条件而可以搜索复用,从而降低验证代价.应用该方法验证了Linux操作系统中SSL协议的实现程序openssl-0.9.6c满足SSL协议的初始握手规范.实验结果表明,该方法具有良好的实用性和可扩展性.

基于语义的启发式智能手机病毒检测与防治方案的设计

随着智能手机的日益普及,智能型手机越来越广泛地被应用在各个层面。与此同时,手机病毒以惊人速度蔓延,针对智能手机等无线设备的威胁也在迅速增加,手机的安全问题越来越受到人们的重视,从手机病毒的定义可以看出手机病毒和计算机病毒有着千丝万缕的联系。文章结合智能手机自身的特点,研究了病毒技术,提出了基于程序语义的启发式智能手机病毒的检测与防治方法。也就是通过语义相关性的检查来判定程序是否属于病毒代码。

程序表示学习综述

为了提高软件的开发效率,目前已出现应用人工智能技术进行智能化开发的趋势,如何理解程序语义是智能化开发中需要重点解决的问题.针对该问题,出现了一系列程序表示学习的研究,程序表示学习可以自动地从程序中学习有用的特征,将特征表示为低维稠密向量,高效地提取程序语义并使用于相应的下游任务.对程序表示学习的研究工作进行综述,介绍了主流的程序表示学习模型,包括基于图结构和基于token序列的程序表示学习框架.展示了程序表示学习技术在缺陷检测、缺陷定位、代码补全等任务上的应用,总结了程序表示学习的常用工具集和测试集.分析了程序表示学习未来需要应对的挑战.