形式语义

摘要： 设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.

摘要： 智能工业系统图标的呈现方式能够影响操作员的视觉认知效率。针对国内外工业系统图标进行指示性、安全性、色彩性等语义研究,分析工业系统图标符号语义与实体的具体关联性。分析可知,类象符号表现为名词性的含义或工作状态;标识符号表现为动作和行为,描述操作员行为的目的性;象征符号主要描述动作图形化,不带引导性;综合性符号主要是由类象与标识结合或者类象与象征构成。根据工业系统图标的语义关联性,设计了十种工业系统图标,并通过语义差异量表问卷形式获取用户反馈。调研结果表明,类象和象征语义表现方式在工业系统图标设计中识别性最强,黄色等纯色促进图形符号警示语义的传达,更有利于提高操作员对不同指示范围图标的识别操作效率。

摘要： 直觉主义逻辑的直观语义(即"证明解释")是直觉主义逻辑建立的基础,它遵循直觉主义的构造性立场,但"构造性证明"这个内涵概念依赖于人们的直观理解。直觉主义逻辑的形式语义更为精致,其中以对话语义为代表的博弈式语义和以克里普克(Kripke)语义为代表的模型论式语义具有代表性。对话语义的构建是满足直觉主义要求的,并且从博弈的角度解读了"构造性证明",它是一种满足直觉主义逻辑直观语义的形式语义。Kripke语义的构建是依赖于"实无穷"的,这是直觉主义所拒斥的;另外,"Kripke有效"利用了赋值函数来定义,这是一种外延定义,与直觉主义逻辑的直观语义有偏离。尽管如此,Kripke语义的认识论解释从认识论视角对直觉主义逻辑形式系统作了解读,为直觉主义逻辑在其他领域的应用开辟了道路,也通过逻辑作为桥梁促进了多学科的交叉研究。

摘要： 直觉主义逻辑的直观语义(即"证明解释")是直觉主义逻辑建立的基础,它遵循直觉主义的构造性立场,但"构造性证明"这个内涵概念依赖于人们的直观理解.直觉主义逻辑的形式语义更为精致,其中以对话语义为代表的博弈式语义和以克里普克(Kripke)语义为代表的模型论式语义具有代表性.对话语义的构建是满足直觉主义要求的,并且从博弈的角度解读了"构造性证明",它是一种满足直觉主义逻辑直观语义的形式语义.Kripke语义的构建是依赖于"实无穷"的,这是直觉主义所拒斥的;另外,"Kripke有效"利用了赋值函数来定义,这是一种外延定义,与直觉主义逻辑的直观语义有偏离.尽管如此,Kripke语义的认识论解释从认识论视角对直觉主义逻辑形式系统作了解读,为直觉主义逻辑在其他领域的应用开辟了道路,也通过逻辑作为桥梁促进了多学科的交叉研究.

摘要： PAR platform is a software platform developed by our research team to support software formality and automated development.The platform fully embodies the advantages of functional abstraction and data abstraction,thus making software development convenient and reliable.The key to achieving this performance is a batch of reusable software components.In order to ensure the correctness and reliability of the whole software platform,it is very important to ensure the correctness and reliability of the software components.In this paper,we select some typical software components in the PAR platform,formalize the semantics of the components in a formal way,and prove the correctness of the components with the help of the Coq theorem prover,hence improving the efficiency of software compoents' formal verification.%PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台.该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件.为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要.选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率.

摘要： BPMN 2.0编排已成为描述业务流程间交互事实上的标准.BPMN 2.0编排面向流的特征,使之会产生控制流方面的语义错误.因此,检查编排语义正确性是BPMN 2.0编排建模工具所期望具有的功能.但是,BPMN 2.0标准规约中的编排缺少形式语义及相应的分析技术,这阻碍了对BPMN 2.0编排的语义分析.提出了一种映射,用于将BPMN 2.0编排转换为工作流网,使用Petri网来形式化定义BPMN 2.0编排的语义.借助Petri网的分析技术,这种定义的语义可用来分析BPMN 2.0编排的结构和控制流方面的锚误.该映射和语义分析已被实现为一种工具.实验结果表明,这种形式化可以识别BPM AI过程模型库中编排的语义错误.%The Business Process Modelling Notation 2.0 (BPMN 2.0) choreography is a de factor standard for capturing the interactions between business processes.Flow-oriented BPMN 2.0 choreographies can exhibit a range of semantic errors in the control flow.The ability to check the semantic correctness of choreographies is thus a desirable feature for modelling tools based on BPMN 2.0 choreographies.However,the semantic analysis of BPMN 2.0 choreographies is hindered by the lack of formal semantic definition of its constructs and the corresponding analysis techniques in the BPMN 2.0 standard specification.This paper defines a formal semantics of BPMN 2.0 choreographies in terms of a mapping to WF-nets.This defined semantics can be used to analyze the structural errors and the control flow errors of BPMN 2.0 choreographies with analysis techniques of Petri nets.The proposed mapping and the semantic analysis have been implemented as a tool.The experimental results show this formalization can identify the semantic errors of choreographies from the BPM AI process model library.

摘要： Vague classes are classes obtained through exemplars and similarity. The usual way we deal with vague objects is using exemplars and the similarity with exemplars. There are mainly two types of vague classes: vague classes with convergent exemplars and vague classes with divergent exemplars.The latter seems more common.For vague classes with convergent exemplars, which are also named as vague classes with core, the borderline cases can be handled by the definition of core. However,since the vague classes with divergent exemplars have no core,the method of core interpretation is un-fit for divergent cases. In actual process of dealing with vague object,both the positive exemplars and the negative exemplars are employed by people. By abstracting the pro-cess, this paper introduces the concept of negative exemplars, and provides a method to deal with borderline cases by using both positive exemplars and negative exemplars. As for the formalized part,based on the first-order languages,this paper give language L?and its semantics by adding positive exemplar predicate,negative exemplar predicate and topic term,In L?,there could be further definition of positive predicate,negative predicate and middle predicate. Through these expressions,the vague objects and their features could be characterized.%含糊类是基于样本和相似性得到的类.通过样本和与样本的相似性处理含糊对象是人们在面对含糊性时常用的方法.含糊类有样本收敛和样本发散两大类型,后者应该更为普遍.样本收敛的含糊类也是有核含糊类,可以通过核来处理边界情况.但是因为样本发散含糊类同时也是无核含糊类,所以这个方法不适用于样本发散含糊类.从人们对于含糊对象的实际处理看,除了用正面的样本外,还会用到反面的样本.将这个过程加以抽象,本文引入了负样本以及提出了由正样本和负样本共同处理边界情况的方案.在形式刻画方面,主要是在一阶语言的基础上通过增加正样本谓词、负样本谓词和论题词给出了语言L?及其语义.在L?中可以进一步定义正谓词、负谓词以及中间谓词,通过这些表达式可以对于含糊对象及其性质给出相应的刻画.

摘要： 为了提高服务消息接口的规范性和交互行为的正确性,提出了一种服务消息交互的元建模方法.基于工作流模型对服务进行建模,通过对消息操作模式予以分析,给出了接口形式化表示和接口相容性检查方法.采用推理规则和递归函数刻画消息传递的语义,讨论了服务交互时各种环境的变化情况.实例分析表明,该方法可以规范服务接口模式,有效地对消息的交互情景进行建模,进而保障服务建模的可靠性.%To improve the normalization of message interfaces and the correctness of interactive behaviors in service,a meta-modeling approach of service message interaction was proposed.Firstly,workflow model is utilized to model service.Then by analyzing the message operation pattern,a method about interface representing and compatibility checking is given.Finally,inference rules and recursive functions are used to describe the semantics of message transmission,and the change of environments is discussed at the same time.Case analysis shows that the proposed method can normalize service interface patterns,model message interaction situation effectively,and ensure the reliability of service modeling.

摘要： 美国著名语言哲学家伯奇提出并论证了“专名是一种特殊的谓词”的观点，以此来批评关于专名在形式语义学中的两种经典观点。本文在评述伯奇的工作及相关争论的基础上试图表明伯奇对“缩略”观点的批判是有说服力的，但对“个体常元”观点的批判却基于对“真正的专名的用法”与“伪专名的用法”的混淆。就“真正的专名用法”而言，将专名视为形式语义理论中的“个体常元”，仍是最有说服力的理论。

摘要： 在形式语义的支持下提出了一种动态工作流建模方法。该方法在扩展UML的基础上给出了两种建模机制，利用UML活动图和状态图对动态工作流过程进行建模。最后，本文给出一个汽车企业产品研发的建模实例说明了本方法对动态工作流建模的有效性。

摘要： 在MAS的分析与设计中,Agent间的交互协议设计是极其重要的内容.特别是交互协议的正确性、有效性和可验证性尤为关键,因此形式化描述和验证多Agent的交互协议非常有必要.定义了用于描述多Agent基于对话的交互协议的一个演算,该演算是基于进程代数的并且独立于Agent的推理过程.该机制可以实现异构多Agent系统的交互协议验证.通过Agent会话环境的状态和演算的形式语义,可以验证会话协议的一些属性,例如:终止性、是否死锁等.该方法可以有效地解决交互协议的语义验证问题,因为协议的状态和Agent的行为由协议本身定义,并且可以避免基于状态搜索的状态空间爆炸问题。

摘要： 本文通过介绍和考察纳入这一语用策略在当代形式语义理论中对解决先设投射问题的作用,揭示其给语义一语用接口带来的某种启示。文章分为四部分：⑴关于纳入策略的有关背景；⑵什么是先设投射问题以及传统解决方法所存在的问题；⑶当代语义理论是如何利用纳入解决先设投射问题的；⑷纳入给语义-语用接口问题带来的启示。

摘要： 为了提高服务消息接口的规范性和交互行为的正确性,提出了一种服务消息交互的元建模方法基于工作流模型对服务进行建模,通过对消息操作模式予以分析,给出了接口形式化表示和接口相容性检查方法采用推理规则和递归函数刻画消息传递的语义,讨论了服务交互时各种环境的变化情况实例分析表明,该方法可以规范服务接口模式,有效地对消息的交互情景进行建模,进而保障服务建模的可靠性.

摘要： 为了提高服务消息接口的规范性和交互行为的正确性,提出了一种服务消息交互的元建模方法基于工作流模型对服务进行建模,通过对消息操作模式予以分析,给出了接口形式化表示和接口相容性检查方法采用推理规则和递归函数刻画消息传递的语义,讨论了服务交互时各种环境的变化情况实例分析表明,该方法可以规范服务接口模式,有效地对消息的交互情景进行建模,进而保障服务建模的可靠性.

摘要： 为了提高服务消息接口的规范性和交互行为的正确性,提出了一种服务消息交互的元建模方法基于工作流模型对服务进行建模,通过对消息操作模式予以分析,给出了接口形式化表示和接口相容性检查方法采用推理规则和递归函数刻画消息传递的语义,讨论了服务交互时各种环境的变化情况实例分析表明,该方法可以规范服务接口模式,有效地对消息的交互情景进行建模,进而保障服务建模的可靠性.

摘要： 为了提高服务消息接口的规范性和交互行为的正确性,提出了一种服务消息交互的元建模方法基于工作流模型对服务进行建模,通过对消息操作模式予以分析,给出了接口形式化表示和接口相容性检查方法采用推理规则和递归函数刻画消息传递的语义,讨论了服务交互时各种环境的变化情况实例分析表明,该方法可以规范服务接口模式,有效地对消息的交互情景进行建模,进而保障服务建模的可靠性.

摘要： 本文给出了一个面向Statechart描述的测试用例集自动生成工具FTCL.FTCL由语法解释器,语义解释器和测试集生成器构成.语法解释器是把一个给定的Statechart描述转换成为精简的可形式分析的8元组结构.Statechart描述可以包含并发和层次的状态结构,以及跨级转换,转换优先级,广播通讯等语法特征.语义解释器负责从8元组结构生成对应的语义模型.本文我们通过区分Statechart描述的外部可观察行为和内部隐含行为提出了适用于测试集生成的可观察语义模型.基于Tretmans在一致性测试方面的研究工作,我们提出了面向Statechart描述的一致性关系,测试集定义和测试集生成器.FTCL是一个年轻的工具在本文最后我们给出了进一步改进的计划.

摘要： 本文给出了一个面向Statechart描述的测试用例集自动生成工具FTCL.FTCL由语法解释器,语义解释器和测试集生成器构成.语法解释器是把一个给定的Statechart描述转换成为精简的可形式分析的8元组结构.Statechart描述可以包含并发和层次的状态结构,以及跨级转换,转换优先级,广播通讯等语法特征.语义解释器负责从8元组结构生成对应的语义模型.本文我们通过区分Statechart描述的外部可观察行为和内部隐含行为提出了适用于测试集生成的可观察语义模型.基于Tretmans在一致性测试方面的研究工作,我们提出了面向Statechart描述的一致性关系,测试集定义和测试集生成器.FTCL是一个年轻的工具在本文最后我们给出了进一步改进的计划.

摘要： 可以使用语义分层结构来分析用户反馈。在一些实例中，用户反馈包括自由形式的文本。用户反馈可以被映射到包括多层级的节点的一个或多个语义分层结构，其中每个节点对应于一个类。一个或多个语义分层结构的信息可以被映射到本体模型。本体模型的映射信息可被用于标识针对用户反馈的可采取操作项(例如，问题、建议、疑问或其他争议)。关于可采取操作项的信息可以提供给个体用于评估可采取操作项。

摘要： 兼具通用语义及领域语义的形式概念相似性快速度量方法，主要用于利用FCA方法进行文本信息检索中的形式概念相似性快速度量，属于信息检索技术领域。为解决现有形式概念相似性判断方法无法包含数据集所涵盖的领域信息问题以及计算内涵语义相似性的过程过于复杂等问题。本发明通过数据集的主题聚类，统计各个词共属类别的次数；利用概念格成员的属性频率和逆概念频率求取基于成员的重要性的两个概念相似性；内涵中每个属性使用基于公共语料的词向量表示，并取其均值作为内涵向量；使用各个词共属类别的次数修正内涵向量的相似性，获得两内涵包含通用和领域语义的相似性；综合基于成员重要性的相似性和内涵语义相似性，得到两个形式概念的相似性。

摘要： 本发明公开了一种基于形式化语义的BPMN2.0执行引擎，该引擎是一个原生BPMN2.0执行引擎，可直接执行BPMN2.0语言。首先，定义BPMN2.0语言的可执行形式化语义并验证其正确性，接着将可执行形式化语义应用于K框架，再融合Z3SMT解析器，实现BPMN2.0语言的可执行引擎。该执行引擎无需转换成第三方语言，节约了检查业务流程模型正确性的人力物力成本。

摘要： 本发明公开了一种面向需求表格模型的形式化语义分析与检查方法，将机载安全关键软件的需求映射为基于命题逻辑与关系理论的数学模型，对其语义进行严格数学定义，然后设计一系列自动化算法来对需求的多层语义约束进行验证。

摘要： 本发明公开了一种语义标签约束的地理信息检索意图形式化表达方法，主要步骤包括：1）结合用户检索需求及认知习惯，概括和抽象地理信息资源检索意图的基本组成要素及其逻辑关系，构建“意图‑子意图‑维度分量”多维多层次的检索意图模型，其中维度分量由维度标识符、关系及正、负标签组成；2）结合相关元数据规范构建地理信息资源检索意图维度树，为意图描述提供参考；3）基于地理本体扩展意图维度分量，对意图进行语义化描述。本发明的检索意图形式化表达方法旨在建立地理信息资源检索意图的统一描述机制，为意图传递与识别提供表示模型，以满足检索需求复杂且表达受限情景下资源精准发现的需求。

摘要： 本发明提供了一种基于Go语言可执行形式化语义的程序漏洞分析方法，包括：(1)对GO语言的官方给出的拓展巴克斯范式进行研究，并结合K框架可支持的BNF语法格式，提出把GO[EBNF]转化为一般巴克斯范式的方法，得到了GO[BNF]；(2)依据GO[BNF]和Go语言的特点，应用K框架，基于重写逻辑，定义Go语言的可执行语义GO[KS]；(3)采用基于测试用例的方法分析GO[KS]的正确性，分别在K框架和IntelliJ IDEA工具中单个执行测试用例，通过比较每个测试用例的结果的一致性来分析语义的正确性；(4)基于K框架，应用GO[KS]，查找Go程序漏洞。本发明提高了Go语言语义的完整性，并实现了对程序漏洞的分析。

摘要： 可以使用语义分层结构来分析用户反馈。在一些实例中，用户反馈包括自由形式的文本。用户反馈可以被映射到包括多层级的节点的一个或多个语义分层结构，其中每个节点对应于一个类。一个或多个语义分层结构的信息可以被映射到本体模型。本体模型的映射信息可被用于标识针对用户反馈的可采取操作项(例如，问题、建议、疑问或其他争议)。关于可采取操作项的信息可以提供给个体用于评估可采取操作项。

摘要： 本发明公开了一种软件函数形式语义及形式化证明脚本自动生成方法，包括：对汇编指令执行后的新系统状态进行构建，使经过指令执行后的新系统状态的每个状态分量均由初始系统状态的状态分量表示；构建所有汇编指令的形式语义函数库；记录在构建被改变状态分量值的表达式树用到的指令语义函数和子路径语义函数，以及表达式化简中用到的化简规则和子路径语义证明定理，自动生成指令执行后新状态的形式语义和相应的形式化证明脚本。本发明能够对输入的微内核操作系统中的一个函数生成汇编代码、生成该汇编代码对应的若干条执行路径信息、对每条执行路径生成相应的形式语义和形式化证明脚本，最终生成自动生成函数的形式语义和形式化证明脚本。

摘要： 本发明公开了一种基于RAPID语言形式语义的机器人控制程序调试方法及装置，该方法包括：对RAPID语言官方提供的语法格式进行分析，并重构为符合K框架规定的传统巴克斯范式；根据RAPID语言的特性以及调试时待观察的程序状态，定义运行配置格式；基于RAPID语言的语法和运行配置，使用K框架定义RAPID语言形式语义RAPID‑FS；基于RAPID‑FS，使用K框架调试机器人控制程序。本发明改变了机器人编程语言缺少形式语义的现状，且为机器人控制程序开发者提供了一种方便、直观的调试功能。

摘要： 本发明公开了一种基于形式语义推理和深度学习的自然语言知识挖掘方法，包括以下步骤：机器学习步骤，用于将形式语义推理和机器学习方法相结合，并进行包含语义的机器学习；意图学习步骤，用于学习待挖掘的自然语言的描述意图；文本主题提取步骤，用于根据LDA模型分析文本主题内容和段落内容描述意图；文档结构分类模型搭建步骤，用于根据深度卷积神经网络进行模型训练，在训练过程中自动修饰完善该神经网络，并搭建自动文档结构分类器。本发明依靠自动化语义推理与深度学习技术与自然语言处理的结合，直接对以文献、语音等为代表的非结构化数据群进行处理并对意图进行推理，以了解文字描述的真实意图，将挖掘和检索到的知识用于新知识结构的分析和构造，从而实现高效、智能与可学习和自演化地进行知识挖掘与检索。