UniNet Description of Dining Philosopher Problem

The UniNet specification of Dining Philosopher Problem we presents not only is graphic and intuitionistic but also explicitly indicates the In the specification, static semantics and the the static properties are dynamic semantics. the recorder of the dynamic properties, and the dynamic properties are the track of the static properties change. Accordingly, Dining Philosopher Problem is formally verified by UniNet. Furthermore, the procedure of properties＇ verification is implemented through the graphic-related computing style.     

Rigorous Modeling of Real-time System Based on UML and PVS

Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in formalization and verification content, and better performance. Time constraints are modeled and verified and its a highlight of this paper.     

An arithmetic of mapping enterprise process metrics to information model based on semantics

This paper analyzes the semantics structure of enterprise process metric and gives guidelines to describe the semantics of metric for collecting metric data automatically. Based on domain ontology, a structure called semantic tree is defined to describe the semantics relationships among measured entity, measurable attribute and constraints, which provides the same method to define semantics of process metrics and data elements in enterprise information model. The arithmetic to map process metrics to enterpr...     

翻译过程中词语弹性的语义阐释

根据语义学理论的基本原理,探讨了英汉词语的核心、外延和认知意义,提出在翻译过程中必须正确把握词语的弹性,才能达到原文和译文之间的“动态对等”。     

图象数据模型研究

数据模型研究是设计按内容检索的图象数据库系统的基础．本文根据图象信息系统的特点，将面向对象模型与超语义模型有机结合，提出了一种新的图象数据模型及相应的说明语言．该模型以紧耦合方式融合了语义数据模型和知识模型的特点，并增加了表示图象对象间空间关系的机制，使得该模型可以更好地描述图象信息系统中的图象数据、领域知识以及空间关系语义．     

基于动态体系结构的形式化描述

随着软件工程的发展,对软件的动态演化提出很高的要求,动态体系结构语言成为描述复杂软件体系结构重要工具.提出基于形式化语言Z的描述,通过Z体系对构件、连接件、配置进行定义,以达到动态演化的目的.     

"否则"的形式语义

作为汉语中的一个二元连接词,"否则"实际上有3个主目,其中的一个被省略掉了.这种省略是依赖于语境的,确切地说,其主要与"否则"之前的子句的主连接词有关.在某些情况下,这种省略是歧义的.基于更新语义框架,本文为"否则"构造一种动态语义.在这个语义中,语句的意义是语义堆上的更新函项,"否则"是更新函项上的二元运算.这种处理方式能够成功捕捉这种省略对于语境的依赖.     

基于元模型架构的UML类图到PVS规范的转化方法

UML是一种非形式化的面向对象建模语言,它缺少精确的语义定义;PVS规范则是一种具有精确语义定义的形式化规范语言,通过PVS规范给UML图形赋予精确的语义可以结合两者的优势.为此,提出了一个将UML类图转换成PVS规范的框架.按照UML的4层架构,依次对元元模型、元模型以及UML图形进行转换,并且前一次转换所得到的规范可以为后面的转换提供上下文背景.与其他方法相比,这种分层转化的方法降低了转换难度,保证了转换的正确性,保持了UML模型更完整的语义成分.     

基于进程代数的上下文感知模型

针对当前上下文感知研究大多集中于技术解决方案，缺乏理论上统一描述模型的问题，提出了基于进程代数的上下文感知模型（CAMBPA）．该模型独立于具体的应用平台，具有平台无关性．首先，利用带时间参量的上下文的状态变迁来描述动态环境的变化，并根据进程代数的合并理论，采用合成简单环境状态变迁的方法来实现对复杂环境状态变迁的描述．随后，通过在模型中引入感知函数，实现了对感知行为的描述，同时对上下文状态变迁赋予了资源语义，从而使模型能够刻画移动计算环境中的动态资源情形．采用染色Petri网对CAMBPA模型实例进行了可视化仿真，结果表明该模型具有语法、语义的正确性，以及良好的可扩展性，能够很好地描述上下文感知．     

基于CTL的并发系统CSP模型验证

主要通过指称语义和回答集程序(Answer Set Programming,简称ASP)完成迹模型的生成,并构建了一套基于计算树逻辑(computing tree logic,简称CTL)的CSP模型验证方法.实验表明,该方法对于分支类型的性质具有较好的描述能力,且保证了验证的正确性.     

产品MBD数据集三维标注中工艺面的形成与校验

由于造型原理、方法等原因,三维模型中的面往往不具有明确的工程语义,使三维模型上标注工程尺寸等信息易产生歧义,目前商用CAD软件没有很好地解决该问题.基于OpenCASCADE几何造型内核研究了解决该问题的方法,提出造型面和工艺面的概念,通过对造型面的数学属性识别,结合机械工程中工程语义,将造型面进行绑定,形成符合工程语义的工艺面,把模型三维标注信息作为工艺面的属性,增加了系统三维尺寸标注的智能性,也为后续的产品虚拟装配、加工制造以及产品服役中语义信息的自动提取提供可能.     

基于UML活动图的动态工作流过程建模的研究

在形式语义的支持下,提出了一种适合动态工作流过程建模的方法.该方法在扩展UML活动图的基础上给出了一种建模机制,利用扩展的UML活动图来对动态工作流的过程进行建模.最后,将该方法用于一个汽车企业产品研发的过程建模实例,且建模结果证明该方法是适合的.说明了基于扩展的UML活动图的工作流过程建模方法对动态工作流过程建模的有效性.     

云计算环境下的SWRL规则分布式推理框架

为解决传统推理引擎在进行大规模OWL本体数据的SWRL规则推理时存在的计算性能和可扩展性不足等问题,提出了云计算环境下的SWRL规则分布式推理框架CloudSWRL.根据SWRL规则语义,并以Hadoop开源云计算框架为基础,设计了OWL本体在HBase分布式数据库中的存储策略,定义了SWRL规则解析模型和相关推理中间数据模型,提出了在DL-safe限制下基于MapReduce的SWRL规则分布式推理算法.实验结果表明,在对大规模OWL本体进行SWRL规则推理时,CloudSWRL框架在计算性能和可扩展性方面均优于传统推理引擎.     

应用SPOM方法辅助获取与分析面向服务需求

In order to design and provide good services,it is necessary for students to describe and understand the customer requirements for services rapidly,to design and plan the services and their behavior,and to schedule service processes effectively.This paper proposes a new service-oriented requirement elicitation and analysis method based on answer set semantic,sketches requirement Meta-model and correlative proofs and algorithms,which can help students represent requirement more declarative and precise.Based on the Meta-model,Subject-Predicate-Object requirement method and specification is presented,by which students can constitute a smooth,small-step,incremental and iterative development process cut in by forms.By applying this method to teach and help students develop service-oriented application,it is clear that it can help students eliminate the miscommunication between developers and users,assure the correctness of the artifacts and make the users active in development cycle.     

鲁棒环境演算中的互模拟同余关系

移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型，移动环境演算是一种广为使用的描述移动计算的形式化模型．针对这种演算的一种改进——鲁棒环境演算，提出了一个新的标号转移系统，并在此基础上引进了一种互模拟同余关系．同时，作为上述工作的应用，给出了一些重要进程等价性定律的简洁证明．     

基于全序语义结构化工作流的研究

针对业务过程的规范化建模问题,研究结构化工作流.证明了基于全序语义的任意工作流均可转化为与其等价的结构化形式,提出了一种结构化工作流代数,并给出了其语义解释模型.在此基础上,形式化地定义了结构化工作流过程和结构化工作流过程函数,从理论上提供了构建规范化、合理化和柔性化业务工作流概念模型的表示方法和操作语言.医疗实例分析证明了结构化工作流理论在过程建模、再造和动态重组中的有效应用.     

结构化面向对象形式规格说明语言OOZS——规格说明测试

自动或半自动实现面向对象形式规格说明的测试不但要求相应的规格说明语言具有严格的形式语义,而且要求使用人员具有较深的数学基础,从而最终影响了面向对象规格说明测试的研究。本文提出了一种测试方法,该方法通过构造测试用例对面向对象形式规格说明的各种特性进行检验,可以较容易地发现形式规格说明中的不一致、不完整之处。