一种基于Petri网的RFID事件检测的形式化方法

无线射频识别(RFID)采用唯一的电子标签识别物理对象,可高速收集大量目标数据.为向各类应用提供语义信息,RFID系统需从收集的数据中检测用户自定义的复合事件.通过提出一种基于Petri网的RFID事件检测方法,引入形式化的ED-net模型描述复合事件语义,并以此为基础实现一种事件检测方法.ED-net模型是对传统Petri网的一种扩展,提供了描述用户自定义类型、函数及表达式的能力,可精确描述RFID复合事件的属性及时域、非时域、参数化等约束条件.通过对RFID事件形式化描述,各种RFID事件可以统一在ED-net模型,并可自动化进行检测处理,避免了不同复合事件间公共子事件重复检测的问题.最后,经过实验测试和分析,验证了该形式化方法的有效性及其优势.

O-表达式的性质定义与规范(英文)

在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式(O-表达式)的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式(stand-alone O-expression,saloe)。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。

程序:物理对象上的操作表达式(英文)

把赋值语句看作物理对象上的操作时,程序就呈现为物理对象上的操作构成的表达式(简称O表达式)。给出了定义O表达式语法的BNF公式,并用公理规定O表达式的语义。主动式的O表达式以计算最终结果为目的,因而相关公理给出的是施行表达式中操作以后的变量与施行之前变量之间的准确依赖关系。反应式O表达式要对外来需求作反应。描述反应的公理规定如何反应。有关通讯的公理要求正确的信息被正确的接受者收到。共享变量公理则给出有关共享变量的性质判断。例子用于说明异步顺序O表达式的性质是如何分析的。

电子商务支付协议认证性的SVO逻辑验证

与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。

操作表达式的Petri网表示(英文)

程序以操作表达式的形式呈现,而其语义则以公理的形式给出。为帮助理解这些公理并作为实现操作表达式的基础,给出了操作表达式的Petri网表示。传统Petri网的库所(place)概念与程序中变量概念有本质的不同,增加了变量概念的Petri网称为C_net。从回顾C_net的基本定义入手,研究操作表达式的网表示。

轻量级无线射频识别认证协议的改进

Kardas等人提出的轻量级无线射频识别(RFID)认证协议(2011年LightSec会议论文集)若遭遇侧信道分析、物理刺探等攻击会导致密钥泄漏,从而使整个协议认证失败。为此,通过将四步认证改为三步认证、引入密钥恢复机制以及改进密钥的使用方式,使协议效率提高,并且便于在多标签环境中扩展。理论分析结果表明,新协议可以防止读写器与标签之间产生异步,抵抗伪造攻击、重放攻击、消息阻塞攻击、中间人攻击,与原方案相比,认证效率更高。

基于模型转换的MARTE顺序图的形式化分析

作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TTS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD,用TTS4SD描述顺序图的形式语义,最后对TTS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法.

基于扩展库所网的工作流过程规约和模式描述(英文)

通过扩展库所的属性,给出了一种新的Petri网模型,用来规约工作流过程和表示工作流模式,并提出了一种称为参数化模式的新模式。通过区别变迁和工作流路由,使得模型中的库所和变迁能够分别表示引擎的动作和需执行的任务。基于传统的Petri网的工作流模型不适合描述工作流过程所代表的行为,因此提出了ST触发规则表达网模型的语义。

基于Petri网的WSCI形式化模型分析

WSCI是一种Web服务组合标记语言,对于一些关键的业务流程,任何设计错误都会造成重大损失,因此有必要为WSCI语言建立形式化模型并给予分析,从而保证正确的业务流程部署。本文主要给出了WSCI的分析方法,基于文献[1]给出了形式化模型,提出了该形式化模型下的一种网融合方法。该方法将表示进程的网模型与其表示例外处理和子流程的网模型进行合并,形成统一的网模型。本文最后还给出了在该网模型下的可达图分析方法,从而达到分析带有例外处理的WSCI形式化模型的目的。

特征模型融合研究

特征模型为特定领域内软件需求的组织和复用提供了有效的手段.为了构建特征模型,领域分析人员要对领域内尽可能多的应用软件进行系统化分析,识别共性和变化性需求,并根据需求之间的依赖关系抽象和组织需求.随着软件系统复杂性的不断提高,特征模型的规模有日益增加的趋势,特征模型的构建也随之成为了一件十分困难的工作,亟需自动化方法的支持.一种可行的方式是将领域内已有的多个特征模型自动融合为一个较大规模的特征模型,并由人工对融合结果进行微调.现有研究提出了6种特征模型的自动化融合方法.文中在现有研究的基础上,提出了一个特征模型融合的概念框架,并根据此框架对6种方法进行了比较和分析.文中还进一步指出了现有研究亟需解决的3个问题,并针对每个问题提出了可能的研究思路和设想.

基于同步网的BPEL建模和验证

Web服务组合是面向服务架构的一个应用,是指将已有的Web服务组合成为新的服务。业务流程执行语言BPEL(Business Process Execution Language)是一种描述Web服务组合的语言。为了保证BPEL描述的Web服务组合的正确性,提出了分层建模和验证的思想,将BPEL流程分为逻辑层和语义层,并分别建立形式化模型和验证方法。这样不仅能保证对流程正确地建模,而且能降低建模和验证的复杂度。在逻辑层,BPEL元素映射为基于同步网的WSL_net模型。畅通性和无冗余变迁性质保证了BPEL流程基本控制流的正确性并避免了资源的浪费。语义层的建模和验证将另文给出。

死路删除语义下的WS-BPEL流程的建模

提出一种新的模型——DPE网,用于描述死路删除语义下的WS-BPEL流程。DPE网中引入了颜色集CTRL和STAT以表示活动执行的状态和并发活动内链接的状态。这在一定程度上降低了模型的规模,从而得到更为直观的模型。基于DPE网,不仅描述了WS-BPEL流程的基本控制流,包括基本活动和各种结构化活动,而且描述了WS-BPEL流程的死路删除语义和较完整的link语义,包括join condition和transition condition。最后,通过一个实例说明了使用DPE网建模WS-BPEL流程,有助于得到更为准确的分析结果。