操作语义

摘要： 为了对话机器人更加智能,用OwlReady2实现具有逻辑推理能力的人机对话系统.OwlReady2是本体论知识管理的描述语言OWL的Python接口,封装了推理引擎HermiT和Pellet,可以进行基于描述逻辑(DLs)的推理.对作为陈述句和疑问句的DLs表达式给出了语义解释,并利用Python的动态编程功能,实现具有推理能力的人机对话系统.为了使用自然语言,还建立了一个文法解析模块.系统通过了简单对话任务的测试,可应用于日常对话和专业领域.

摘要： 正规函数表是一类典型的Tabular表达式,被广泛应用于软件说明文档.文中对Tabular表达式中正规函数表操作的语义进行研究.首先给出了正规函数表的形式文法,讨论了规整性、完全性和不可交叉性等性质,说明了其求值过程;然后根据操作的影响范围,以内部操作和外部操作为分类标准,分别对二元操作、替换操作、提取操作和扩展操作的语义进行刻画,讨论了各个操作的封闭性;最后通过电梯控制系统实例分析了相关操作的实际应用场景,说明了正规函数表操作的形式语义的合理性和可用性.实例结果表明,文中提出的正规函数表操作的语义描述与实际结果是一致的.

摘要： Formal semantics of UML sequence diagrams is critical to express the dynamic interaction of software system accurately.Therefore,a well-formed sequence diagram is a prerequisite for the analysis and verification of UML model and an important guarantee to improve the reliability of software systems.In this paper,different methods used in UML sequence diagram's semantics were summarized and compared based on the working mechanisms and pros&cons,respectively.Meanwhile,the special issues with respect to how to define the semantics of UML sequence diagram were discussed as well.Finally,some specific research topics and directions in this area were suggested and proposed.%为UML顺序图构建形式化语义,不仅有利于精确描述软件系统的动态交互过程,而且有利于进行基于UML模型的分析和验证,是有效提高软件系统可靠性的重要保障.结合近年来国内外对UML顺序图形式化语义的研究工作,分类阐述了各种方法,综合分析和比较了不同方法的工作机制和优缺点,指出了定义UML顺序图语义时需重点关注的问题.最后,对未来的研究工作与研究思路进行了梳理与展望.

摘要： 针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换后的代码的可接受性以及代码本身较高的可信性.

摘要： This paper introduces a formal verification of mJava compiler targeting Micro-Dalvik virtual machine (VM)where m Java is an object-oriented language similar to Java,and Micro-Dalvik is a Dalvik-like VM of the register-based architecture.The operational semantics of m Java and Micro-Dalvik VM are defined.The compiler operates in two sta-ges.First it replaces the names of local variables by their corresponding indices and hence translates mJava into an intermedi-ate language.Then it generates the Micro-Dalvik VM instructions.After defining the operational semantics of the intermedi-ate language,the correctness of the two stages are formulated in terms of the preservation of the semantics and is proved re-spectively.The whole formalization is machine-checked in the theorem proof assistant Isabelle/HOL.The m Java language and Micro-Dalvik VM are more abstract than the comparable Java and the Dalvik VM,respectively,which is a result of a compromise between the the realism of the language and the clarity of the formalization.However,mJava language and Mi-cro-Dalvik VM exhibit core features of an object-oriented programming language and a register-based architecture,respec-tively,and thus in this sense,this verified compiler is non-trivial.%针对类Java的面向对象语言m Java到类Dalvik的寄存器架构虚拟机Micro-Dalvik 的编译验证，给出了m Java语言和Micro-Dalvik的操作语义．从m Java语言程序到Micro-Dalvik虚拟机指令的编译分为两步，首先将m Java语言程序中的本地变量名转换为相应的序号，得到一个中间语言程序，再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序．在给出中间语言的操作语义后，构造了m Java语言程序与编译后的中间语言程序的语义保持定理并证明，以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明．整个形式化编译验证在定理证明助手Isabelle／HOL中进行了机器检测．m Java语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象，是我们兼顾语言的真实性和形式化的清晰性的结果．但是，所有形式化的语义严格遵从语言规范中的定义，并与Dalvik VM的实现保持一致，从这种意义上讲，该编译器并不是一个实验性质的假想编译器，而是有其实用意义的．

摘要： 安全苛刻系统的可信性需求迫切,支持可信性评估的数据主要来自于测试.为了保证测试数据的可靠性和正确性,特别是对安全苛刻系统这类复杂系统,手工测试实际不可行.研发测试语言是实现自动化测试的有效途径,也是安全苛刻系统自动化测试发展的必然趋势.针对安全苛刻系统通用测试语言应独立于具体设备包括被测安全苛刻系统、测试设备的应用需求,对安全苛刻系统测试中的测试设备协同语句展开研究.针对安全苛刻系统测试中测试设备协同任务中的高阶性、实时性等特点,通过给出测试语言中测试设备协同相关类型、设备协同表达式,定义测试设备协同语句,并通过设备协同表达式求值定义设备协同语句的操作语义规则.最后,对语句的正确性给出相关证明,从而支持安全苛刻系统测试过程中测试设备协同过程的动态性和开放性,支持安全苛刻系统测试语言的通用性.

摘要： 无线传感网的发展,使其需要具有高效地更新其上运行的应用软件的能力.为了解决这个问题,提出了一种面向无线传感网应用重编程的逻辑式编程语言及其处理系统ReLog.ReLog语言根据无线传感网应用的普遍特点,基于传统逻辑式语言进行扩展,并提供合适的编程抽象,方便程序员高效地构建、修改程序.同时,语言的处理系统使用中间代码将应用程序与系统软件解耦,从而减少应用更新时所需传输的更新代码的规模,提高更新效率.通过一个数据收集应用案例评估了ReLog语言及其执行机制,结果表明:使用ReLog语言能够获得简洁、易修改的程序;同时,语言的执行机制能够显著降低传输应用更新代码的能量和时间开销.

摘要： The characteristics of cyber physical systems such as cyberization, systematization and informationization make the software systems more and more complex. Because the classic modeling methods cannot satisfy the needs of Cyber-physical System(CPS), the Spatio-Temporal Consistence(STeC) language for real-time systems whose core property is the consistence of time and location is introduced to model the real-time systems. In order to achieve the automatic logical reasoning in STeC, the equation and rewriting rule in Maude are applied to convert the STeC system to an executable specification description, it can analyze the result of computation and check the correctness of time in the system. Instance results show that the formal description language Maude can effective for real-time system for security verification.%信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此，引入实时系统的规范语言STeC，用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题，通过拓展Maude中的关系等式和重写规则，将STeC语言转化为可执行的基于Maude的形式化描述，使用Maude自动推导功能，自动推导出系统的时间正确性。实例结果表明，该形式化描述语言Maude可有效对实时系统进行安全性验证。

摘要： 面向对象语言在软件工程实践中有着广泛的应用.为面向对象语言定义严格的语义有助于理解面向对象语言的本质特征,对验证软件、提高软件系统可靠性等也具有重要意义.给出了一种新的面向对象语言的语义框架,该框架基于命令式的风格,具有操作语义和类型规则；证明了该语义框架的类型安全定理.%Object-oriented languages have wide applications in software engineering practice, and designing a rigorous semantics framework for these language has great importance in understanding their key features, and also in software verifications etc. This paper presented a new imperative-style semantics framework for object-oriented languages. This framework includes the operational semantics and a type system. This paper proved the soundness theorem.

摘要： Automatic test case generation is an important guarantee to achieve automated testing and to verify the trustness of software. After analyzing the existing methods of automatic test case generation, we propose a compiler-based error-traceable method to generate the test cases automatically. This method relies on the compiler and inserts the test requirements into the source codes properly by expanding the existing syntax and semantics of the source codes. Therefore, when the code generator generates the object codes, it can generate simultaneously the test cases according to the results of the testing requirement analysis. This method unifies the test case generation and the object code generation and brings them in the compiler. By doing this, we can avoid the overhead of information transferring interface commonly included in the situation, in which we develop a single automatic test cases generator that uses the information of another compiler's analysis. At the same time, when the test case cannot pass, it is very convenient for the programmer to correct the errors of their codes because the error positions can be found quickly by the error tracking information of the source codes. Finally, a sample program illustrates the concrete process of this method and proves that the method is effective.%测试用例的自动生成是实现测试自动化的重要保障,是验证可信软件的基本方法.在分析现有测试用例自动生成方法的基础上,提出了一种基于编译的错误可跟踪的测试用例自动生成方法.该方法以编译器为依托,通过对其语法和语义进行扩展,将测试需求很好地融入到源程序中参与分析,并利用代码生成器在生成目标代码的同时根据相应的分析结果直接生成对应的测试用例.该方法将测试用例和目标代码生成统一到编译器中,避免了独立的测试用例自动生成工具在获得编译器相关分析结果时而导致的接口开销.同时,通过对源程序行号信息的跟踪,使得测试用例在无法通过测试时能够很快定位出错位置,以方便程序开发者修改.最后,通过一个示例程序说明了该方法的具体实现过程,证明了该方法的有效性.

摘要： 如何快速、直观地设计出线束工艺图纸一直是线束生产企业需要重点解决的难题。利用通用CAD系统进行线束设计缺乏特定领域所具有的语义,无法精确地表达设计意图。本文基于操作语义的思路,重点研究了线束构件的各种几何约束,提出了一种操作语义的模型结构,并且对其解析算法进行了详细的描述,在此基础上,开发了线束工艺设计系统。

摘要： 提出对基于OWL-S描述的语义Web服务操作语义的Petri网描述新方法。选择动态描述逻辑的动作理论作为语义Web服务描速的逻辑基础,一个OWL-S原子进程可以作为一个动态描述逻辑动作进行描述,实现了对OWL-S原子进程的动态执行争相关执行条件静态逻辑推理的有机结合,进一步通过将Petri网与动态描述逻辑的动作理论结合,得到OWL-S进程(尤其复合进程)操作语义的Petri网描述,为组合语义Web服务的自动组合和动态性质分析提供了更为有效的逻辑依据和方法。

摘要： 对语义Web服务的操作语义进行恰当的形式化描述和有效建模是语义Web服务得到实际应用必须解决的基础问题,尤其是机器如何自动得到语义Web服务的逻辑模型.该文在对语义Web服务操作语义的Petri网描述方法的基础上,通过对原子语义Web服务的OWL -S进程描述进行解析,得到语义Web服务原子进程动态执行相应的Petri网关联矩阵,进一步通过Petri网的自动共享合成操作,得到语义Web服务操作语义的Petri网描述,解决了语义Web服务自动建模的问题,为语义Web服务的动态组合提供了有效的技术依据.

摘要： 工作流中的过程定义、解释执行以及管理监控等相关技术能很好的解决测试管理环境中测试流程定义、测试流程解释执行及监控等相关问题,文中首先分析了软件测试过程模型目前无法满足需求的情况和工作流技术的特点,提出了基于工作流的方法,采用基于XML的测试流程模板定义和存储方法,应用操作语义来描述软件测试过程实例,最后给出了系统的设计和实现过程.

摘要： UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.

摘要： 本文通过组合状态转换Monad和异常处理Monad来定义纯函数式语言文件系统操作,给出了文件系统操作的操作语义.

摘要： 可以将用于RESTful操作的访问控制提供给集中式语义图存储。另外，可以在资源树数据库中分布的语义三元组上提供操作。在示例中，系统可以使用在分级资源树机制中分布的语义描述符来维护语义描述符关系信息。这些机制使得能够在特定图的上下文内通过一起使用特定的一组语义描述符来执行语义查询。为了语义操作目的而使用组的形成的机制还使得能够使用组资源以便向组成员扇出语义请求，组成员包括位于不同服务实体上的成员。

摘要： 本公开是关于一种ICU多设备语义互操作的数据传输系统及方法，包括：数据采集层，用于采集各类医疗设备和传感器上传的数据；数据转换层，用于对上传的各类格式数据进行解析和提取，并以标准格式组织，将标准格式化后的数据上传至边缘计算层；边缘计算层，用于对所述医疗设备上传的标准格式数据进行二次加工，将产生的额外必要数据附加到原始数据包中上传至云端存储层；云端存储层，用于存储所述边缘计算层发送的数据包。本申请以统一的顶层本体架构和标准化术语实现多设备交互，且在数据传输过程中只需要将流程结果和一些原始数据发送到云端存储层中，从而有效的减小网络拥塞和响应时间，提高数据的传输速度。

摘要： 方法、系统和装置，解决与语义推理操作相关的问题。能够基于应用需求定义不同的定制或用户定义的规则，即使这些规则基于相同的初始事实，也会导致不同的推断事实。

摘要： 本发明涉及视频操作点记录语法和语义，描述了用于处理可视媒体数据的系统、方法和装置。一个示例方法包括：根据格式规则在可视媒体数据和包括存储可视媒体数据的一个或多个比特流的一个或多个轨道的可视媒体文件之间执行转换；其中，可视媒体文件包括操作点记录和操作点组框，并且其中格式规则指定：对于可视媒体文件中指示的每个操作点，在操作点记录和操作点组框中包括指示色度格式的第一元素、指示比特深度信息的第二元素、指示最大图片宽度的第三元素和/或指示最大图片高度的第四元素。

摘要： 本公开是关于一种ICU多设备语义互操作的数据传输系统及方法，包括：数据采集层，用于采集各类医疗设备和传感器上传的数据；数据转换层，用于对上传的各类格式数据进行解析和提取，并以标准格式组织，将标准格式化后的数据上传至边缘计算层；边缘计算层，用于对所述医疗设备上传的标准格式数据进行二次加工，将产生的额外必要数据附加到原始数据包中上传至云端存储层；云端存储层，用于存储所述边缘计算层发送的数据包。本申请以统一的顶层本体架构和标准化术语实现多设备交互，且在数据传输过程中只需要将流程结果和一些原始数据发送到云端存储层中，从而有效的减小网络拥塞和响应时间，提高数据的传输速度。

摘要： 本发明公开了一种数据转换操作语义的可视化方法及装置、电子设备，包括：为数据转换操作挑选含有二维数据表的图形图符模板；根据数据转换操作，确定用于展示在二维数据表上的行和列；从真实表格中挑选出与数据转换操作语义相关的行列单元格数据，并填入二维数据表中；在二维数据表的外围填入与数据转换操作语义相关的非真实表格数据；为所述二维数据表中的单元格进行颜色的编码；用标记框将二维数据表中具有依赖关系的列框选出，并用连接线相连；根据真实表格的行列数目大小，为二维数据表绘制行列滚动条。本发明采用多种视觉通道从不同维度可视化数据转换操作的语义，具有通用性广、可扩展性强、可解释性高等优点。

摘要： 本发明公开了一种基于变异操作语义稳定性的API误用缺陷检测方法，针对API误用类缺陷，本发明利用特定的变异操作对待检测的代码注入可能的API误用错误，再利用正确代码中多次注入不同误用错误其语义稳定性要高于已存在API误用错误的代码，来区分正确代码和存在API误用错误的代码，从而达到检测API误用缺陷的目的。本发明的主要内容包括：1)提出了一个基于变异操作语义稳定性的API误用缺陷检测整体流程；2)提出了一种从源代码中提取API调用序列的方法；3)提出了一种针对API调用序列的基于变异操作的API误用错误注入方法；4)提出了一种基于自编码器的API调用序列语义特征编码方法；5)提出了一种基于相似语义归一化的语义稳定性评估方法。

摘要： 本发明提供了一种协同设计中维持关联操作语义一致性的方法，其特征在于：将关联操作分解为本地操作及全局操作；操作转换框架中，添加两个操作历史序列，将关联操作、本地操作分别存放在两个操作历史序列中，存放全局操作在已有操作历史序列中，三个操作历史序列维持关联操作和分解操作关联关系；释放远程编辑操作后，执行消解以前冲突步骤和避免将来冲突步骤，其中，“撤销-转换-执行-转换-重新执行”（Undo-VT-Do-VT-Redo）过程被引入到操作转换策略框架中，用于控制远程操作的执行过程，避免将来冲突步骤：某个全局执行操作所对应的本地执行操作将被应用虚拟转换函数并被重新执行，更新本地内存空间。

摘要： 本发明涉及一种基于原子操作语义描述的多源二进制代码一体化翻译方法，具体含有如下步骤：步骤1：将源平台的机器指令进行反汇编后得到汇编指令，设计原子操作描述语言，对构成指令的指令原子操作及原子寻址方式分别进行描述，组成刻画指令语义的表达式序列，实现对不同处理器指令集的统一描述；步骤2：为简单后续翻译，将不方便处理的表达式序列映射为三叉语义树；步骤3：采用分层迭代的指令语义等价转换算法，在三叉语义树上通过自顶向下的策略进行分层翻译，然后，利用本地编译器产生目标平台的机器指令；本发明了提供一种可扩展、应用范围广、效率高的基于原子操作语义描述的多源二进制代码一体化翻译方法。

摘要： 本发明提供一种基于文件操作语义异步复制的方法，系统设置有文件监控模块、信号过滤器等模块，其中文件操作监控模块监控存储池内文件的变化，当文件改变时，文件操作监控模块捕获语义信号，无效信号被信号过滤器过滤，经过滤的文件操作信号传输到复制策略管理模块，复制策略管理模块根据信号更新策存储池信号临时表；当实例复制策略被满足后，触发快照模块对相应的存储池进行快照操作并将快照信息和信号临时表中的数据更新到信号表，并清空信号临时表；复制策略管理模块启动远程复制模块操作，发送成功后，复制策略管理模块更新信号表中RemoteReplicationStatus为真，完成远程复制。