CC—高阶通信系统的并发演算

并发演算CC(Concurrent Calculus)是高阶并发通信系统的数学模型,它把λ-演算作为子理论并包含一阶通信系统演算CCS、活动进程演算CMP、和高阶通信系统演算CHOCS的主要特征。在CC中,通信端口可为任意表达式并且进程和通信端口都可以作为在通信中传递的一等对象(First-class Objects)。从而CC不仅可以描述一阶通信行为而且可以刻划通信网络的动态自修改行为。另外,由于CC把λ-演算和进程演算纳入同一形式系统,故CC可以作为并发函数式程序设计的核心语言和理论模型。本文首先给出CC的语法、语义和例子,然后研究CC的高阶双向模拟等价关系以及CC的代数定律。最后简单讨论了相关的工作和今后的研究方向。     

一个说明语言的设计和其子集编译器的开发

基于软件文档可执行的想法，设计了一个适用于指称语义描述的可执行规范说明语言——ＪＺＣ，并对其核心子集编译器进行了设计与开发。该语言设计采用了模式匹配、类型并置和构造函数等概念，使得抽象文法易于在程度中体现。模块概念的引入使得函数型语言书写的程序更加易懂和易于编写。作为对严格开发方法的一个尝试，ＪＺＣ核心子集编译器的开发采用了该种方法，其中一个“结果正确性定理”的证明是开发过程的重点工作。本文通过一个示例语言简介ＪＺＣ的语言特点，给出了编译器开发过程的一个描述框架和证明梗概     

混合系统的形式化验证

结合混合系统的研究对余度管理系统进行了形式化的分析和验证.采用的手段是时段演算技术及其扩展.首先进行形式化的需求分析,需求及其假设用时段演算表示,其次严格化地描述算法和参数的选取.在验证过程中,首先应用程序逻辑验证算法,算法的不变量以时段演算表示,最后在时段演算中验证整个系统的行为满足给定的需求.      

基于Petri网的UML状态图的形式化模型

提出一种可以准确描述UML状态图动态特征的形式化模型SC_Net.首先给出了UML状态图的形式化语法定义,其中用状态集合、转移集合、事件集合、条件集合、活动集合、对象集合和变量集合,定义了一系列辅助函数描述UML状态图特征,用确定目标状态和受限源状态表示层次关系,用开放事件和封闭事件表示对象之间的消息.基于C_Net定义了描述UML状态图动态语义的Petri网模型SC_Net,既能描述状态图中的控制部分,又能描述状态图中的数据处理部分,并给出了从UML状态图到SC_Net的转换步骤,便于实现自动转换过程.最后以柔性制造系统的一个实例说明SC_Net能用于分析UML状态图的性质.      

基于语义相似度计算的航天标准关联度评价

随着航天领域各级各类标准编制数量的逐年递增,相关标准之间的交叉重复制定问题随之而来。为解决该问题,文中通过计算语义相似度的方法开展航天领域标准名称、标准范围及主要内容的关联度评价。算例分析结果表明,该方法可以有效评估标准间的关联程度。     

一种基于语义的Ontology映射方法

O n to logy映射是实现异构O n to logy互操作的有效方法,目前的O n to logy映射主要采用句法方法,而很少采用语义方法。本文提出了一种基于语义的O n to logy映射方法,该方法考虑了O n to logy中的概念属性,采用概念名称相似性、概念属性集合相似性、相关概念集合相似性等确定O n to logy之间的语义映射关系;采用语义半径提高了语义映射方法的灵活性。试验分析表明:该方法得到的映射的准确率和查全率在90%以上,准确率和查全率均优于S-M atch方法。该方法已在基于知识需求的主动式知识系统原型中实现,并在某研究所得到了应用。     

Σ-演算的范畴模型

Σ-演算是并发演算CC的子理论,集中体现CC中的并行运算部分的特征。本文将并发通信系统看作是由状态加变换构成的动态系统,建立了Σ-演算的范畴模型(Categorical ModeI),其基本思想是:把Σ-演算中的公式对应于范畴构造中的对象(Objects),Σ-演算中的推演对应于范畴中的态射(Morphisms),从而通过Σ-演算的结构操作语义自然地得到一种范畴结构。这种方法可以推广到其它并发理论之中,例如网论和逻辑方法(如线性逻辑Linear Logic),从而范畴论可以作为描述并发、通信和非确定性行为的统一的形式化框架。     

基于Event B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.     

“只得”和“不得不”的用法辨析

副词"只得"和"不得不"均表示动作行为的执行违背了行为人的意愿。但是两者的语义环境却是不同的:前者是基于选择的多元化,而后者则是对外力强制下执行动作的将就[1]。因此它们在用法上也呈现出了一定的差异。