基于UPPAAL的简单网络支付协议形式化验证

分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息,在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷。新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境。     

一种基于时间自动机网络的实时系统形式化验证方法

介绍了时间自动机形式模型,在此基础上给出了时间自动机网络的形式语法和语义,然后给出一种基于时间自动机网络的实时系统形式化验证方法,并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．     

基于UPPAAL的铁路车站信号联锁系统模型验证

详细介绍了适于描述实时系统的形式化方法,时间自动机以及基于时间自动机的模型验证工具UPPAAL.给出了铁路车站信号系统中的联锁功能进路建立的时间自动机模型,并利用UPPALL对其进行了分析与验证.     

UPPAAL环境下通讯协议的自动验证

对UPPAAL环境下通讯协议的规范验证方法进行研究,在此基础上,利用一组时间自动机模型模拟一个具有严格时间限制的网络通讯协议,并对其正确性进行自动验证.     

一种优化的智能合约模版生成方法

针对业务流程智能合约部署到以太坊时Gas成本消耗问题,设计了一种优化的业务流程智能合约模版生成方法.通过将业务流程BPMN模型扩展为Petri网后,利用Petri网的化简规则进行化简,找出BPMN模型中可以视为融判任务的节点组合后,对原业务流程BPMN模型进行化简.提出一种BPMN模型到Solidity智能合约代码的映射规则,将化简后的业务流程BPMN模型翻译为优化的智能合约模版.经过以太坊部署测试,验证了优化的智能合约模版能够降低智能合约部署时的Gas消耗.     

基于双通道的智能合约漏洞检测方法

智能合约因漏洞而造成巨大的经济损失受到了广泛关注。针对现有的智能合约漏洞检测方法检测精度不高的问题,结合动态卷积神经网络(dynamic convolution neural network,DCNN)、双向门控递归单元(bidirectional gate recurrent unit,Bi GRU)、图传递神经网络(message passing neural network,MPNN)、注意力机制提出了基于双通道的漏洞检测方法DBTA(DCNN-BiGRU-MPNN-Attention)。首先利用Word2vec词嵌入技术和图归一化方法对数据进行预处理,将获得的词向量表示传入改进DCNN-BiGRU,并引入了R-Drop(regularized dropout for neural networks)正则化方法提高模型泛化能力。将图归一化表示传入图传递神经网络,通过两个通道分别提取序列特征和图特征,然后结合自注意力机制和交叉注意力机制捕捉不同特征间的相关性,从而突出关键特征对漏洞检测的重要性。最后通过全连接层得到输出向量,利用sigmoid函数输出结果。通过消融实验和对比实验表明...     

智能合约设计模式

针对以太坊Solidity语言智能合约设计问题,在研究开源合约程序的基础之上识别了面向智能合约的六种设计模式,包括访问约束、状态机、前置条件、后置条件、紧急制动和代理。面向智能合约的设计模式有益于提升合约代码可读性,降低合约语言学习难度,也是提高区块链合约代码审计效率的途径。     

基于层次时间自动机的移动授权的建模与验证

基于通信的列车运行控制(communication based train control,CBTC)系统以其安全、可靠等性能优点在城市轨道交通的运营中得到广泛关注。它通过其核心功能,即为每一列通信列车提供移动授权(movement authority,MA),来实现列车安全间隔运行。针对功能安全和实时性等方面的不足,首先,建立移动授权的层次时间自动机(hierarchical time automaton,HTA)模型,其中嵌入了列车管理、安全位置、遍历障碍物和列车筛选模块,并对模块间的交互信息进行分析;其次,采用巴科斯范式(Backus-Naur form,BNF)语法对其特性进行描述;最后,利用UPPAAL对各特性验证。结果表明,移动授权模型满足实时性、顽健性、可用性、完整性、安全性5项需求,层次时间自动机理论适用于系统需求规范的验证。     

基于UPPAAL的虚拟生产系统仿真

虚拟生产系统(VPSs)是一种为应对易变的和不确定的制造环境而提出的新型生产资源结构形式.针对VPSs的特点,提出了基于自治与协调机制的控制结构.应用赋时自动机理论以及在UPPAAL的辅助下,对VPSs进行了DEDS的建模.为获得期望的性能(生产流程和时间)和行为特性(避免冲突和死锁),设计了基于启发式调度规则的自治与协调监控器,并进行了系统分析和时间最优调度的计算与仿真,从而构建起兼顾控制和调度问题的VPSs闭环监控系统.     

基于迁移学习的智能合约漏洞检测方法

针对智能合约源代码漏洞数据集匮乏的问题,提出一种基于迁移学习的智能合约漏洞检测方法.首先,从CodeBERT预训练模型中迁移表示传统编程语言的语义特征参数,学习智能合约编程语言Solidity的语义表示;其次,使用长短期记忆网络处理语义向量,加入上下文语义关联;最后,训练智能合约漏洞检测模型,完成智能合约源代码形式的二分类漏洞检测任务.实验结果表明,与基线方法和机器学习方法相比,该方法在数据集匮乏情况下的智能合约漏洞检测准确率更高.     

基于LSC的形式化验证方法

调查研究了LSC在形式化验证方法中的作用的研究发展现状,包括LSC在从系统行为需求描述转换形成模型检验的系统行为模型中的作用的研究现状,LSC在抽取待验证系统性质的作用的研究现状,LSC在模型检验中的作用的研究现状,展望了LSC在未来模型检验中的发展方向——概率模型检验.     

基于胶囊网络和注意力机制的智能合约漏洞检测方法

近年来,随着智能合约的数量越来越多,因合约漏洞而造成的经济损失愈发严重,智能合约的安全性越来越受到广泛的关注。基于深度学习的漏洞检测方法能够解决早期传统智能合约漏洞检测方法检测效率低、准确率不足的问题,但大多现有基于深度学习的漏洞检测方法都是直接使用智能合约源代码、操作码序列或字节码序列作为深度学习模型的输入,会因引入过多无效信息而削弱有效信息。为此,文中提出了一种基于胶囊网络和注意力机制的智能合约漏洞检测方法。考虑到程序的执行时序信息,文中通过提取智能合约的关键操作码序列作为源代码特征,然后利用胶囊网络和注意力机制的混合网络进行训练,其中胶囊网络模块用于提取智能合约的上下文信息以及局部与整体的联系,注意力机制用于给不同的操作码按照其重要程度分配不同的权重。实验结果表明,文中提出的算法在智能合约数据集中的F₁分数和准确率分别为94.48%和97.15%,与其他传统检测方法和深度学习方法相比有较明显的性能提升。     

构件化嵌入式软件设计的能耗性质分析与验证

从嵌入式软件设计模型层对构件化实时嵌入式软件系统中能耗相关性质进行研究,包括:扩展了实时接口自动机在能耗语义方面的描述能力,通过引入状态能量消耗率,建立了能耗接口自动机形式化模型以及自动机网络,用以建模嵌入式软件设计阶段系统构件及其构件组合的能耗行为特征;对能耗接口自动机网络的状态空间进行了形式化分析,构造了相应的可兼容整型空间的可达图,并在此基础上给出了最小能耗计算和最大能耗验证的算法.     

基于区块链智能合约的电力供应链利益分配研究

首先构建电力直接交易供应链参与者的利润函数,然后利用区块链智能合约构建电力直接交易供应链利益分配模型,并根据分配因子自动匹配利益并结算,进而实现电力直接交易供应链上各个企业利益实现最优的同时保证整个供应链利益最优.算例表明:该模型能够使得电力直接交易供应链维持稳定.     

基于稀疏优化的智能电表误差估计方法

【目的】利用改进动态线损和稀疏优化方法研究智能电表运行误差估计。【方法】首先,考虑电表误差的稀疏性,加入稀疏正则项,对动态线损模型进行改进,提高误差估计的精准度;进一步地,利用交替方向乘子法改进设计迭代算法,交替求解改进动态线损模型,获取智能电表误差估计结果。【结果】利用Matlab和实际数据进行数值仿真实验,验证所提方法的有效性。【结论】通过分析线损率与计量误差估计的耦合关系,提高了误差估计的精度。与动态线损模型对比,本文所提方法的检测准确率更优。