一种基于有限精度时间自动机的模型检测工具

基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。

基于Groebner基的模型检测技术及其工具实现

为了减少运算复杂度和运算时间,优化检测的性能,使得计算过程更加快速高效,在符号化模型检测的过程中,利用G roebner基进行多项式约化,设计出新的模型检测算法。并且基于该算法开发出新的符号模型检测工具。该工具能更快速地验证各软件及硬件系统的性质,具有较高的实用价值。

模型检测在软件需求分析及设计中的应用

模型检测技术因其完全自动化并且验证速度快的优点在硬件及协议的验证中广泛应用,近年来在软件领域的应用研究也不断涌现。总结了模型检测在软件需求分析及设计中已有的应用技术,包括利用模型检测工具对RSML,SCR和UML图形的检测,以及直接的模型检测,并从不同角度对已有技术进行系统的分析和比较。最后对该项技术研究的方向进行展望。

RGPS过程层元模型正确性验证

利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。

智能合约的形式化验证方法

智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.

自动验证参数化Leader Election 协议

讨论了一类Leader Election （LE）协议，该类协议通常运行在允许进程随时加入或崩溃的动态环境中，给出了LE协议的参数化版本，即考虑分布式系统中的进程数目任意多的情况。并提出了一种自动验证参数化LE协议的方法，用线性算数约束来模拟可能无限的全局状态集合，利用符号模型检测工具DMC[DP99]， 文章实现了对参数化LE协议safety性质的自动验证。

无人机无线通信协议的形式化认证分析与验证

针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人机节点以及各个无人机节点之间的身份认证;运用模型检测工具SPIN验证无线通信协议的一致性,其中提出一种改进的知识项获取方法,加快攻击者需掌握知识集的求取过程;验证结果表明该无人机无线通信协议具有中间人攻击漏洞。