基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

为提升拍卖合约时间安全性验证效率及验证公平性,提出基于角色的拍卖合约抽象建模及其验证方法。首先,对合约源代码进行基于账户角色的抽象建模,转换为时间自动机网络模型,并对时间安全性进行形式化描述,用UPPAAL工具验证。其次,提取合约源代码机制,建立智能合约机制模型,同样转换为时间自动机网络模型,并对4种公平性进行形式化描述,再用UPPAAL验证。最后,通过2个经典案例证明了所提方法的可行性和有效性。

沉浸式虚拟现实多模态交互模型研究

随着虚拟现实技术的发展,鼠标和键盘等传统输入模态已经难以满足沉浸式虚拟现实交互需求,如何使用自然交互方式来满足沉浸式交互任务日益成为研究热点.为了实现自然高效的人机交互,该文首先分析各种单模态交互方式的优缺点,并基于神经科学和运动学的角度划分视线转移;其次,结合头动的稳定性与眼动的高效性以及头眼协调特征设计了一个头眼协调交互模型,通过多模态相互作用减少Midas误触和识别用户意图;最后,针对虚拟现实的目标选择任务进行模态对比实验.实验结果表明:与传统交互模态相比,该交互模型具有更高的精度、更快的时间效率和更高的自然度.

PAR平台中若干软件构件形式化验证技术研究

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。

虚拟现实软件系统开发方法研究

虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得十分庞大和复杂,涉及许多多媒体数据。传统软件开发方法和程序设计技术侧重于处理文本数据,显然不能满足开发虚拟现实软件的需要。试图以所在团队研发成功的PAR方法和PAR平台为基础,根据虚拟现实软件系统的特征,探寻虚拟现实软件系统开发的新方法,进一步扩充和完善PAR平台中已有多媒体处理技术、形式化建模技术和C#等高级语言程序自动生成系统。

无线射频RFID识别协议自动验证方法研究

Population Protocols是一种受生物启发的计算模型,能够表示无线网络中数量庞大但计算能力弱的多组件间的交互,它为无线传感器网络提供了一种可计算推理的理论框架。将Population Protocol理论引入到RFID识别协议中,提出了RFID识别协议系统模型验证框架;构建了标签与阅读器交互产生的状态变迁模型;最后用spin模型检测工具和LTL线性时序逻辑验证了弱公平条件下该模型的自稳定性,为分析与验证无线传感器网络中协议的正确性提供了一种行之有效的方法。

邻域粗糙集中不确定性的熵度量方法

针对传统粗糙集理论中不确定度量方法难以适用于邻域粗糙集模型的问题,引入信息熵的度量方法,提出了基于信息熵的邻域粗糙集不确定性度量方法。该方法采用邻域关系对连续型数据进行信息粒化,基于粒化后的数据定义邻域系统中的近似精度、邻域信息熵、加权邻域信息熵等不确定性度量。进一步提出邻域系统不确定性度量的公理化表示,证明邻域系统的近似精度、邻域信息熵、加权邻域信息熵都是公理化度量;给出其最大最小值,证明其满足单调性原理。理论分析与实验表明邻域系统中的信息熵度量优于近似精度度量。

二进制粒计算模型

粒计算是一种处理不确定性数据的理论方法,涵盖粗糙集、模糊集、商空间、词计算等。目前,数据的粒化与粒的计算主要涉及集合的运算与度量,集合运算的低效制约着粒计算相关算法的应用领域。为此,提出了一种二进制粒计算模型,给出了粒的三层结构,包括粒子、粒群与粒库,并定义了二进制粒子及二进制粒子的运算,将传统的集合运算转化为二进制数的计算,进一步给出了二进制粒子的距离度量,将等价类的集合表示方式转化为粒子的距离度量表示方式,给出了粒子距离的相关性质。该模型定义了二进制粒群距离的概念,给出了二进制粒群距离的计算方法,提出了基于二进制粒群距离的属性约简方法,证明了该方法与经典粗糙集约简方法的等价性,并以二进制粒群距离作为启发式信息,给出了两种约简算法。

在建模语言Apla中实现多媒体数据库应用的方法研究

随着信息技术在各大领域的广泛应用,产生的多媒体数据所占比例越来越大,对多媒体数据处理的需求也越来越多,高级程序设计语言支持多媒体数据处理的功能也变得尤为重要.采用模型驱动的思想,在支持模型驱动软件开发PAR平台的Apla→Java程序自动生成系统中,扩充对多媒体数据处理的功能,并提出多媒体数据处理机制和Apla中基于关系代数的文本处理机制自然融合,包含了对多媒体数据处理的Apla语言程序,可以通过Apla→Java程序自动生成系统自动转换成等价的Java程序,使得Apla语言具有对多媒体数据处理的能力.

Transaction在PAR平台中的实现方法及应用研究

随着电子商务和金融软件应用日益广泛,提高这类软件系统的可靠性和安全性就显得特别重要。虽然能够提高这类软件可靠性的事务处理技术早在数据库管理系统中普遍使用,近几年在Java软件开发环境中也新增了事务处理接口JTA,但是在基于模型驱动架构设计的建模语言中嵌入事务处理机制的成功案例尚不多见。论文在已有体现模型驱动软件架构思想的PAR方法和PAR平台中,融入抽象事务处理机制,并使用融入了事务处理机制的PAR平台及其建模语言开发了具有事务处理功能的金融软件模型,通过PAR平台的模型自动转换工具生成了Java和SQL程序。实验证明融入了事务处理机制的PAR方法和PAR平台具有建模简单、实用,软件开发效率高,便于形式化推导和证明等特点。

Apla→Java程序生成系统中泛型机制实现方法研究

在对泛型程设本质特征深入研究的基础上提出了新型泛型语言机制构想,并在Apla→Java生成系统中具体实现的新方法.该方法比现有的Java、C++、C#等语言中泛型机制的实现方法简单,并通过经典算法实例演示实现效果,大量用例的成功测试表明该实现方法的可靠性和新型泛型语言机制的正确性.

跨媒体组合方法研究

大数据时代以多媒体计算为基础的跨媒体计算技术已成为信息技术研究的热点。但是,对跨媒体的获取、组合和应用仍缺乏有效的方法。提出了两种跨媒体组合方法。以开发跨媒体在线二叉树遍历课程为例。第一种方法以Web服务的模式,引用多种类型多媒体数据,将其以服务组合的方式进行拼接,从而构成跨媒体服务。第二种方法是基于本实验室团队自主研发的PAR平台中的"New SQL"技术与Apla语言程序,使用PAR平台的多媒体数据库技术实现对跨媒体数据的存储和检索,进而构成Apla语言程序,实现部署在云端的多媒体服务,有效地解决了跨媒体的组合与存储问题。

PAR平台中并发分布式事务处理机制及其应用研究

随着大数据、云计算和云服务等新技术的兴起,并发分布式计算作为这些新技术的基础,扮演着越来越重要的角色.在分布式计算中,数据的一致性难以得到保证,而事务处理技术能够有效解决该问题.为了提升PAR平台在高可靠应用程序的使用范围,在其建模语言Apla中融入了并发分布式事务处理机制,使得Apla语言不仅支持分布式数据库事务,还支持分布式非数据库事务.该文对Apla语言并发分布式事务处理机制进行了深入地研究,并将其应用在学生管理系统、在线购物系统等实际应用场景中.

新型Action泛型机制在PAR平台中的实现和应用研究

在软件开发过程中,开发语言中的泛型机制能够显著提高软件开发的效率和软件可靠性,但现有高级语言中一般只有类型和子程序(如过程、函数和方法等)作参数,限制了泛型机制的应用.该文对新型泛型机制进行深入探索,着重研究以action作为参数的泛型机制.在Apla→Java程序自动生成系统中实现了将Web服务作为Apla语言中的action参数的泛型机制,完善了Apla语言中的泛型安全的约束机制,成功地将新型泛型机制应用于PAR平台中.

基于Apla语言的虚拟现实建模机制研究

针对传统的脚本建模存在语言机制复杂繁琐、开发效率不高、可靠性难保证、建模阶段和交互阶段相互独立等问题,基于分划与递推(PAR)及其Apla抽象程序设计语言,设计与原Apla语言融合的虚拟现实建模语言机制。开发的Apla→MAXScript自动生成系统可以将抽象Apla程序转换成MAXScript脚本,并借助3DSMax来实现三维建模。Apla建模机制采用直接重用MAXScript修改器API方式,既大幅度简化了重构的工作量,又延续了Apla语言抽象程度高特征,便于对Apla建模程序进行形式化推导和正确性验证。最后通过案例证明了Apla建模语言及其工具能够提高三维建模的精细度、可靠性及开发效率。