基于优化目的的人机界面知识化表示方法

对一种新的人机界面操作和交互行为的知识化表示方法进行了介绍和分析。以语义网络为基础,通过对人在界面操作中的知识作业过程及交互行为进行分析研究,建立了一种带距离标识的基于面向对象的语义网络的界面知识化表示方法,提供了人机界面特征集定义、推理规则和交互描述模型。该表示方法从界面语义模型和心理语义模型的角度描述了交互,能够正确地描述人机界面的语义知识特征。并以手机短信界面为例说明了该方法的有效性和必要性。     

基于关系／网状的语义超图多媒体描述模型

本文提出了基于关系／网状的语义超图功述模型及各操作，引和面向对象的方法，统一描述对象和元组，提出了对象间的语义联系，基于联系的各种操作和施加工对象的方法机制。在语义超图层次，描述和操作了不同语义类的对象；在语义子图层次，描述了每一语义类的对象间的多对多关系及其操作，因此，该模型可用于描述和处理工程领域中的不同语义类多对多关系的复杂多媒体对象。     

基于结构化操作语义的安全协议分析框架研究

操作语义模型是一种用来分析安全协议的新模型,它以操作语义学为基础,结合了多种协议分析模型的优点,能直接分析多个协议的组合问题.本文在对安全协议操作语义模型进行研究的基础上,构建了一个基于结构化操作语义的安全协议分析框架,给出了该框架中的协议规格,协议运行,威胁模型和安全性质等形式化定义.最后,以经典的Needham Schroeder Lowe 协议为例,用该分析框架分析了其机密性和认证性.     

协同CAD系统中操作语义共享技术研究

研究了协同CAD系统的操作语义,给出了操作语义的定义和描述方法、操作语义的识别技术以及基于本体的映射模型,在此基础上提出了一种基于操作语义共享的CAD协同框架,最后给出了基于该框架的一个原型系统。     

基于结构模型的人运动图像语义描述

人运动图像语义的研究是对人运动图像中人体运动行为的一种描述方法,通过其语义来实现图像的识别与检索。该文希望通过对人体运动的几种较为简单的动作语义的研究,来开启对人运动图像语义的全面研究。为了实现该目标,提出了基于模型的人运动图像的语义描述,即模型语义,模型语义具有直观性、推导性和可行性。通过定义基本模型和语义操作规则,建立一个语义的形式描述理论,此模型语义是人运动图像语义全面研究的基础。     

基于本体的决策模型冲突预测及协商研究

依据模型知识的特性,定义了模型描述本体和任务求解本体,为模型提供语义支持.模型语义分为描述语义和行为语义.基于描述语义的相似性判定,模型可进行潜在冲突预测;然后根据任务求解本体的定义,模型通过行为语义交互,进行行为协商;而在执行过程中,模型需要为每一个操作申请资源,因此模型根据模型描述本体和描述语义对资源申请进行协商,从而得到互不冲突的操作执行序列,消除冲突.最后通过实验分析验证算法的有效性.     

基于语义传递的分层事务调度技术的研究

传统的读写事务模型是面向机器的，即事务的每个操作都是对数据库的存取操作，并且事务只有两层：逻辑层和物理层；逻辑层描述对逻辑数据的操作，如对记录的修改，查询等。物理层是描述对磁盘页面的操作；因此，它不能有效地描述应用程序的语义，本文提出了一个３层事务模型，在传统事务模型的基础上增加了一个语义层，该层能有铲地描述应用环境的各种语义，为事务处理提供语义信息。同时设计了基于这种事务模型的并发控制机制，该机     

一种用于类C语言环境的安全的类型化内存模型

使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证.     

PCF的信息系统模型

带类型的λ－演算是一个逻辑系统，它可以作为程序语言的基础．Ｐｌｏｔｋｉｎ所引进的ＰＣＦ就是这样一类程序语言．Ｐｌｏｔｋｉｎ构造了ＰＣＦ的一个模型，然后讨论与这个模型相关的指称语义和操作语义之间的配合问题──简单配合和完全配合．本文利用Ｓｃｏｔｔ引进的信息系统概念构造ＰＣＦ的另一种模型，并证明与这个模型对应的指称语义与操作语义是完全配合的．     

语义特征建模系统中操作局部化的研究

为了提高语义特征建模系统约束求解的效率及系统的整体性能,提出了一种新的操作局部化方法。该方法使用特征语义表示法来描述产品模型中特征的各种信息,改进了细胞元模型对特征元素的管理机制,通过特征的“语义面”将局部特征从模型中有效地分离出来,通过创建临时特征的方法来实现模型的局部约束求解。该策略不仅可以完全满足在复杂模型中直接操作的需要,还可以大大提高系统的性能。实验表明该算法具有更强的适应性和实用性。     

Algebraic approach to linking the semantics of web services

Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models, respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.     

Semantics of plan revision in intelligent agents

In this paper, we give an operational and denotational semantics for a meta-language of the 3APL agent programming language. With this meta-language, various 3APL interpreters can be programmed. We prove equivalence of the operational and denotational semantics. Furthermore, we give an operational semantics for object-level 3APL. Using this semantics, we relate the 3APL meta-language to object-level 3APL by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3APL.     

Towards a theory of mathematical operational semantics

Turi and Plotkin gave a precise mathematical formulation of a notion of structural operational semantics in their paper “Towards a mathematical operational semantics.” Starting from that definition and at the level of generality of that definition, we give a mathematical formulation of some of the basic constructions one makes with structural operational semantics. In particular, given a single-step operational semantics, as is the spirit of their work, one composes transitions and considers streams of transitions in order to study the dynamics induced by the operational semantics. In all their leading examples, it is obvious that one can do that and it is obvious how to do it. But if their definition is to be taken seriously, one needs to be able to make such constructions at the level of generality of their definition rather than case-by-case. So this paper does so for several of the basic constructions associated with structural operational semantics, in particular those required in order to speak of a stream of transitions and hence of dynamics.     

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems (STS), etc. However, there is little research about the equivalence between these semantics. In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transformthem to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.     

Logical approximation for program analysis

The abstract interpretation of programs relates the exact semantics of a programming language to a finite approximation of those semantics. In this article, we describe an approach to abstract interpretation that is based in logic and logic programming. Our approach consists of faithfully representing a transition system within logic and then manipulating this initial specification to create a logical approximation of the original specification. The objective is to derive a logical approximation that can be interpreted as a terminating forward-chaining logic program; this ensures that the approximation is finite and that, furthermore, an appropriate logic programming interpreter can implement the derived approximation. We are particularly interested in the specification of the operational semantics of programming languages in ordered logic, a technique we call substructural operational semantics (SSOS). We show that manifestly sound control flow and alias analyses can be derived as logical approximations of the substructural operational semantics of relevant languages.     

Linear-Time Self-Interpretation of the Pure Lambda Calculus

We show that linear-time self-interpretation of the pure untyped lambda calculus is possible, in the sense that interpretation has a constant overhead compared to direct execution under various execution models. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use a self-interpreter based on previous work on self-interpretation and partial evaluation of the pure untyped lambda calculus.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term (using the same operational semantics).By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation (similar to graph reduction) and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.     

A rewriting logic framework for operational semantics of membrane systems

Existing results in membrane computing refer mainly to P systems’ characterization of Turing computability, also to some polynomial solutions to NP-complete problems by using an exponential workspace created in a “biological way”. In this paper we define an operational semantics of a basic class of P systems, and give two implementations of the operational semantics using rewriting logic. We present some results regarding these implementations, including two operational correspondence results, and discuss why these implementations are relevant in order to take advantage of good features of both structural operational semantics and rewriting logic.