精华内容
下载资源
问答
  • 现在市场上出现了一些一键式的智能合约形式化验证工具,据说可以最大程度的减少验证程序、发现bug,提高工作效率。这种一键式的智能合约形式化验证工具真的有效么?为了求真笔者做了一个测试。 本次笔者测试选择的是...

    在智能合约的形式化验证过程中,需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。现在市场上出现了一些一键式的智能合约形式化验证工具,据说可以最大程度的减少验证程序、发现bug,提高工作效率。这种一键式的智能合约形式化验证工具真的有效么?为了求真笔者做了一个测试。

    本次笔者测试选择的是成都链安研发的离线版免费验证工具Beosin-VaaS。我们基于VSCode的插件市场安装一个sodility开发插件(具有语法检测,高量和语法联想,方便合约开发。),安装完成后,在插件市场安装成都链安的免费检测工具Beosin-VaaS。
    合约代码如下:
    在这里插入图片描述
    在这里插入图片描述
    我们用成都链安的插件检测一下我们合约中存在的问题
    在这里插入图片描述开始检测
    我截取部分报错解释说明一下
    插件报错会展示行号和那一行的代码以及描述信息,有助于开发人员修改问题
    在这里插入图片描述
    在调用call/send函数后无论执行成功还是失败都不会直接抛异常,如果不对调用返回值进行检查,函数会继续执行,造成安全漏洞。
    在这里插入图片描述

    溢出是典型的合约漏洞,可能导致检查被绕过,合约运行逻辑出错。
    在这里插入图片描述
    Solidity中允许有未使用的变量,它们不会构成直接的安全问题,但会降低代码的可读性并且额外占用存储空间导致部署时的资源消耗增加。
    在这里插入图片描述
    成都链安的检测插件集成了编译器的告警,会提示你一些合约开发中的信息。
    在这里插入图片描述
    在transfer、transferFrom、transferOwnership等敏感函数中,用户操作不可逆,所以建议开发者在这些函数实现中增加目标地址非零检查,避免用户误操作导致用户权限丢失和财产损失。

    以上是我们这个合约中部分存在的漏洞报错,有了这个插件的检测,我们就能快速定位解决问题,使我们的合约更加安全。

    展开全文
  • Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础,能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证,帮助构建功能正确,安全,可靠、可信赖...

    在这里插入图片描述

    Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础,能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证,帮助构建功能正确,安全,可靠、可信赖的系统。

    OneSpin 360™2020.2.0版本现已准备就绪,该版本包括功能和性能方面的改进。新增与增强的功能有:

    ● 新的编译器和优化程序:这些改进了工具所有部分的性能,包括更快的工具启动,设计编译和GUI交互。

    ● 新的FSM指示器:如下所示,此新指示器提供了更高级的界面来调试和理解FSM。它允许按状态过滤状态,并且能够交互式地自定义状态布局。

    在这里插入图片描述

    ● 新的形式化引擎:新引擎在履行设计限制的同时,其行为就像是随机模拟器。它可以很好地按顺序解决深度属性,并且在某些属性上已证明比现有引擎快300倍以上。与以前的默认引擎设置相比,它还可以在属性检查上并行运行,可检查的属性数量增加了10倍以上。

    ● 对SystemC附加构造的支持:扩展的构造支持包括自动插入等待状态以打破循环。

    新版发行的具体内容如下:

    OneSpin 360™常用功能的新功能

    ▷ 支持VHDL物理类型“时间”。
    ▷ SystemVerilog类支持已得到改进。
    ▷ SystemC现在支持C++ 14,包括std::array和std::tuple。所有从C++到14的语法改进,例如SCIN < ScIt< 10 >的双角括号也可用。
    ▷ 大大提高了编译命令的运行时间,运行效率的改善高达几个数量级。

    图形用户界面中的新功能

    ▷ 从2020.2版本开始,FSM表中的状态可使用拖放手势。手势生成的是所有onespin shell命令可接受状态的字符串类型名称。

    ▷ 通过上下文菜单功能增强了属性调试器。自该版本发布以来,信号可以被跟踪,添加到波形中或在其他查看器中显示。

    ▷ 从此版本开始,打开代码查看器后,调试器的响应能力明显包括了新的触发器类别。信任问题管理器中的问题现在可以从视图中排除与/或导出到CSV。状态机的死锁情况现在会在信任问题管理器中报告。

    OneSpin 360™设计验证的新功能

    ▷ 新的随机模拟引擎:disprover6。这个新引擎已添加到用于坚持和整数检查的默认配置中。也可以添加到prove配置中。例如:“check -prover_exec_order {{approver2 disprover6}} my_property”。

    ▷ 现在可以直接创建SVA模块,而无需使用create_sva_module -no_read_sva读取。

    ▷ 改进了截断和固定溢出检查的显示名称。例如:“ @ truncation @@ / local/TEST/dut.sv@16:1”到“ truncation_check_1”。

    ▷ 覆盖关闭加速器(CCA)应用程序已增强了与受支持模拟器的集成。

    ▷ FPU应用程序现在支持生成溢出异常以转换为整数。

    ▷ 处理器架构和验证应用已发布。

    ▷ 信任评估平台(TAP)应用程序具有以下增强功能:默认情况下,不会报告冗余分配带来的可靠性问题。运行analyze_trust -category reliability_assign指令以观察问题。信任问题管理器现在已自动启动。如果查看器关闭,则可以使用launch_trust启动报告视图,新命令export_trust可以用于生成CSV文件以进行脱机处理/分析,analytics_trust包括新的触发器类别。可以将信任问题管理器中的问题排除在视图之外与/或导出到CSV。

    360 EC-FPGA的新功能

    ▷ OneSpin 360™现在包括针对以Max 10目标器件为目标的Quartus Prime Standard™实施流程的全面综合验证支持。

    ▷ 通过Virtex、Kintex和Zynq系列芯片对Xilinx Vivado的综合验证支持现在包括对状态的自动映射,其中Xilinx Vivado™生成的netlist名称依赖于分配的范围。此外,OneSpin 360™ 现在已经改进了分布式ram的状态映射,比如RAM32M和RAM64M内存块。

    ▷ OneSpin 360™的新指令analytics_clock_mapping,可通过查找映射到非时钟的时钟来帮助用户确定错误的设计设置。

    ▷ OneSpin 360™具有一项新功能,实现相同功能的映射RAM会被自动黑盒,这是一个抽象的概念,它可以显著提高可伸缩性。

    ▷ OneSpin 360™现在提供工具认证套件与实施流一起使用,该实施流是基于Synopsys Synplify™(G-2012.09A-SP4版本)进行合成和MicroChip Libero IDE™(9.2版本)反熔丝芯片(SX-A™、eX™、MX™和Axcelerator™系列)。

    OneSpin 360™常用功能的已修复问题

    ▷ 修正了在调整FSM表格的大小期间可能偶尔发生的显示问题。

    ▷ 修复了一些窗口可能被缩小为零的问题。现在,所有窗口和选项卡都具有最小尺寸。

    ▷ 新的FSM可视化GUI。更好的FSM气泡默认设置以及交互式重新排序。可用的过滤器可以更好地可视化状态。

    局限性

    ▷ Windows版本不支持OneSpin 360 DV的并行验证。这意味着尽管验证器并行工作,但不支持多个断言的并行运行(set_ check_option -local_processes)。也不支持通过网络进行证明分布(set_ check_option -parallel network)。这些选项被接受但被忽略。此外,Windows版本不支持GUI中的HTML选项卡。对于生成HTML输出的应用程序,如quantify或visualize_fsm,需要一个外部浏览器。

    ▷ 由于Windows平台上不存在Verdi™,因此Windows版本不支持在Verdi中进行调试或从FSDB读取初始状态。

    ▷ 如想要在Windows上验证SystemC,需进行64位Cygwin的最新版本安装。此外,软件包mingw64-x86_64-gcc-g ++必须安装在7.4.0版本中。

    ▷ 如在Linux系统上验证SystemC,必须安装软件包libstdc +±devel。

    -版权所有,抄袭必究-

    更多信息:http://www.softtest.cn/

    展开全文
  • Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础,能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证,帮助构建功能正确,安全,可靠、可信赖...

    目录

    OneSpin360图形界面

    一致性检查举例

    等价性检查举例


    Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础,能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证,帮助构建功能正确,安全,可靠、可信赖的系统。

    本文基于OneSpin 360版本 2020的学习笔记

    OneSpin360图形界面

    OneSpin360读入了设计后,它的图形界面如图1所示。图中三个数字标红的圈圈是OneSpin360提供给用户的主要功能。用户可以方便的通过这些按钮去实现其功能。其中标红圈圈1中,主要是用于用户执行设计设置 (Design Setup):

    • 读入设计(Reading in the design :VHDL button for VHDL files, V button for Verilog files)
    • 详细阐述设计(Elaborate the design : E button)
    • 编译设计(Compile the design : C button)
    • 指定时钟信号和复位时序(Specify clock pins and reset sequence)

    图1 OneSpin360 图形界面

    在design setup 结束后,用户可以切换到三种模式,CC、MV和EC. 此后,先前组成setup模式的按钮将会被隐藏并显示当前模式的按钮。如图2中显示的是setup模式,从左到右的按钮的功能依次是读入VHDL文件、读入Verilog文件、设计详细阐述(elaborating the design)、编译(Compiling)、设计和端口(pin the port ,only EC mode)。右边三个是模式选择。

    图2 setup 模式

    红色圈圈2是shell/message/progress 窗口,每个功能的输出信息都会显示在这里。命令在shell 窗口输入红色圈圈3功能如下:

    • Hiding the shell -隐藏shell 窗口,进入GUI 模式
    • Hid the GUI – 隐藏GUI, 进入shell 交互界面
    • Interrupting the execution of a running command - 中断操作命令
    • Calling the help browser – 调用帮助手册

    OneSpin 提供了非常强大的帮助命令,这很方便用户很快的查找命令和掌握该工具,很大的方便了验证师,节省了验证时间。那么如何获得帮助呢? 除了在GUI界面下直接点击help-browser外,用户可直接在OneSpin shell区中输入命令“help”。Help命令可以获得对一个命令的详细语法描述。例如,以下命令都可以获得read_verilog命令的语法描述:

    Setup> help read_verilog

    Setup> help *verilog*

    除help命令以外,OneSpin shell也支持使用Tab键自动匹配(Tab-completion)命令。当用户输入了命令的前几个字母,再按下Tab键,如果输入的前几个字母在命令中是唯一的,shell就可以自动输入该命令;如果不唯一,shell就会列出所有匹配的命令,用户可以通过上下键自由选择,例如(图3):

    setup>read_

    Tab-completion的功能不光适合于命令匹配,在命令的选项(option)和文件名的匹配上同样适用。

    用户要退出OneSpin时,可以在shell中输入:exit.如果用户没有保存数据库(database),oneSpin就会弹出对话框,提示是否保存数据库。

    图3 Tab 键自动匹配命令

    一致性检查举例


    在这里用一个小例子来说明如何用OneSpin来执行一致性检查(consistency checking).

    • 步骤1:随便找一个vhdl 或者verilog 文件,我这里是这一个VHDL文件包含了整个设计文件。
    • 步骤2:Read the Design

     在shell 窗口使用以下命令读入设计文件,-version 93是指定VHDL标准

    Setup > read_vhdl -cell   -version 93 arbiter.vhd

    也可以在GUI界面,点击setup 目录下的VHDL,其中version可以选择VHDL的标准。点击文件后Read & close 就可以,会在shell 窗口提示读成功

    • 步骤3:Elaboration and Compilation

    在读入全部的VHDL 和Verilog 文件 之后,必须对设计座elaboration,在shell 窗口输入:

    Setup > elaborate

    对于时钟,复位以及一些黑盒或者其他不关心的设计,用户可能通过一些特别说明来阐述。这个后面再讲。详细设计阐述后就可以compile 了,这个命令会产生一些单元的内部描述,见图4。

    Setup > compile

    图4完成编译后的OneSpin界面

    • 步骤4:set mode to CC

    OneSpin有三种可选的模式,在CC(consistency checking)模式和 MV (module Verification)模式下都可实现一致性检查(consistency checking)。这种重复是因为一致性检查是非常有用的。而且便于用户集中注意力在等价性检查(equivalence checking),而不需要360MV许可证(License)。所以非常值得推荐。

    为了进入一致性检查,可在shell窗口中输入下面的命令:

    Setup > set_mode cc

    Tips: 该命令会将命令提示符从” setup”转变到”cc”,如图5所示。

    图5 CC 工作模式

    • 步骤5:一致性检查 consistency checking with model building assertions,在CC模式,执行命令check_consistency:

    CC > check_consistency

    许多的基本检查会被自动执行。这些检查都是基于设计中插入的一些断言实现的。在工程应用中,该功能一般很少用到。所以这里不做详述。执行完一致性检查后,便可以开始执行模块验证(module verification)或者特征检查(property checking)。这个后面再说。一致性检查结果会再shell 窗口打印如图6

    图6 一致性检查打印结果

    一致性检查包含了signal domain checks 、init checks、fsm checks、dead code checks、stick checks; 如果只需要对其中某一项进行检查可以使用命令(如init checks):check_consistency  -category { init } 除此之外,还可以再GUI界面操作,如图7所示,check ALL Visible 就是检查所有可见的条目,另外通过explain Check可以查看本条检查的规则。Explore Selected Auto Check 可以定位到这条检查在设计中的位置。

    图7 GUI界面手动检查

    等价性检查举例


    这部分主要举例说明如何用OneSpin执行等价性检查(equivalence checking)。等价性检查主要是检查两个门级网表(gate-level netlist)之间是否一致或者RTL级与门级网表级是否一致以及两个RTL描述是否一致。在此,将以前一部分提及例子的VHDL设计作为对比举例。

    1.Read the two design

    在OneSpin中,被比较的两部分设计被冠以象征性的名字‘‘golden”和“revised”。通常,假设gold design是正确的,把revised design 和golden design 进行对比。为了强制某一命令工作在golden design 或者revised design上,必须指定相应的选项-golden或者-revised。如果投有指定这些选项,系统将默认当前的设计是golden design, 命令也将会工作在当前的设计。通过命令读入两个VHDL 文件

    Setup > read_vhdl -golden arbiter.vhd

    Setup > read_vhdl -revised arbiter_new.vhd

    读如上述两个文件后的OneSpin界面如图8所示:

    图8 读入两个文件后的OneSpin界面

    2.Elaboration and Compilation

    在读入设计文件之后,必须要做elaboration和compile.

    Setup > elaborate -both

    Setup > compile -both

    编译成功后,OneSpin 会产生两个设计(golden 和 revised)的内部描述(internal representation : unit model)

    图 9 Elaborate 和Compile之后界面

    3.Set Mode to cc

    成功编译后,就可以进行等价性检查了(equivalence checking),在shell 窗口输入命令:

    Setup > set_mode ec

    4. Map Pins and States

    设计的对比以golden design 和 revised design 的输入、输出和状态的映射(mapping)为基础。它们的映射关系通过map 命令建立起来,完成映射后的OneSpin界面如图10所示:

    ec > map

    图10 EC 模式下map 之后的OneSpin 界面

    5. Compare the two design

    在建立了映射(mapping)之后就可以对两个设计进行对比了,在ec 模式下上输入命令

    ec > compare

    该命令会将所有的映射的输入和状态(compare point),并且输出的结果概述。对于那些行为不同的对比点,将会产生一个反例。图11为OneSpin 完成对比之后的界面。

    图11 完成比较之后输出信息

    6.Debug Differences

    对于每一个失败的状态,都可以通过GUI中双击各自的状态得到一个反例,此外,GUI还会显示失败的fanin view.这些信息有利于调试。

    7.Fix bugs

    可以通过edit_file 命令还编辑有bug的文件,需要注意的是在文件修改之后,revised design 必须要重新读入,编译,映射对比。

    展开全文
  • 近期,笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓**“离线免费版”,相较于之前该公司推出的在线免费版、企业版而言,亮点自然不言而喻。对于开发者来说,离线版的验证工具将提供...

    形式化验证工具之离线免费版Beosin—VaaS

    近期,笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓**“离线免费版”,相较于之前该公司推出的在线免费版、企业版而言,亮点自然不言而喻。对于开发者来说,离线版的验证工具将提供一个不联网的测试环境,在很大程度上能从根源上将黑客攻击的可能拒之门外。
    在这里插入图片描述
    经笔者测试,虽然这次推出的版本为免费版,但功能毫不逊色,依然能
    有效检测出智能合约的常规安全漏洞,并精确定位到有风险的代码位置,以及导开发者修改合约代码。**对大多数智能合约的安全性而言,需求都已经满足。在此附体验网址:https://beosin.com/#/,有需要的朋友可自行前往体验。

    尽管笔者认为离线免费版Beosin—VaaS的功能已足够强大,但根据官方发布的消息,对于一些复杂类型的业务合约、以及对安全性要求高的业务合约,比如数字金融类(如DeFi)、物流供应链类、跨境支付类、防伪溯源类等等,还是建议选择企业版Beosin—VaaS人工审计服务更好。

    下面笔者将针对这款离线免费版Beosin—VaaS工具进行简单展述。

    1.什么是形式化验证技术?

    其实,形式化验证技术最早是应用于航空、军事等领域的安全关键软件中的技术,本身受众范围没那么广。当成都链安最早尝试将形式化验证技术应用在验证智能合约的安全性上,最后发现审计效果比起传统的验证方式,更具备优势。

    **形式化验证技术是一种基于数学和逻辑学的方法。**具体来讲,在智能合约部署之前,对其代码和文档进行形式化建模,然后通过数学的手段对代码的安全性和功能正确性进行严格的证明,可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。

    该方法可有效弥补传统靠人工经验查找代码逻辑漏洞的缺陷,其优势在于,用传统的测试等手段无法穷举所有可能输入,而用数学证明的角度,就能克服这一问题,提供更加完备的安全审计。

    2.什么是Beosin—VaaS工具?

    Beosin—VaaS相关工具就是将形式化验证技术应用在对智能合约安全性验证的集大成者。Beosin—VaaS能够面向EVM和WASM智能合约,自动化检测智能合约的10大项32小项常规安全漏洞,为智能合约提供**“军事级”的安全保护**;并精准定位风险代码位置并给出修改建议;检测准确率>97%,全球最高;从源码到字节码完备的形式化验证;支持多个智能合约编程语言,如Solidity、Go、C++、Python等。

    3.一些Beosin—VaaS的测试实例

    笔者选取了655个测试问题进行检测,Beosin—VaaS工具总计检测出635个问题,命中率为96.9%;误报共115个,误报率为15.3%。因此,Beosin—VaaS工具可检测出业务类大多合约案例,具体检测项如下:

    Beosin—VaaS工具检测项

    漏洞检测项 Beosin—VaaS工具
    ERC20 标准规范
    Fake Recharge Vulnerability(假充值)
    TransferToZeroAddress(目标零地址检测)
    Re Entrancy(重入)
    TXOriginAuthentication(tx.origin使用错误)
    Invoke Low Level Calls(call调用,delegatecall调用,自杀函数调用)
    BlockMembers Manipulation(区块参数依赖)
    Invoke Extcodesize(调用Extcodesize函数)
    Invoke Ecrecover(调用Ecrecover函数)
    Unchecked Call Or Send Return Values
    (call和send的返回值检测)
    Redefine Variable From Base Contracts(合约继承中的变量覆盖)
    Unprotected Ether Withdrawal(无保护的转账) ×
    Check This Balance(合约资金受到严格限制)
    ArbitraryJumpwith Function(具有函数类型变量的任)
    Overload Assert(重写assert函数)
    CompilerVersionDeclaration(编译器版本声明)
    Constructor Mistyping(构造函数失配)
    Unary Operation(+= 写成=+ )
    No Return(返回值适配)
    Unchecked Api Return Values(没检查API返回值)
    Emit Event Beforerevert(事件在revert前触发了)
    Integer Overflow(整数溢出)
    Exception State(异常检测,包括数组越界、除0、assert失败等))
    Call problem
    Function problem
    Require Fail

    通过大体测试,离线免费版自动形式化验证工具Beosin—VaaS在很大程度上都能够满足大多数开发者的验证需要。大家可以前往https://beosin.com/#/进行体验,不吝赐教。

    展开全文
  • 11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin—VaaS,该版本基于流行的开发工具VSCode插件,供广大开发者免费使用。获得方式如下...
  • PAT工具全称是Process Analysis Toolkit,可以做一些简单的验证。 今天我们分析一下例子里面的Monty Hall Problem 这个问题不知道大家知不知道,这里简单介绍一些这个问题(羊车门问题)。话说有一个国外的电视...
  • 今天学习一下Perterson Algorithm. 这个算法是使用三个变量来实现并发程序的互斥性算法。 具体看一下代码: Peterson算法是一个实现互斥锁的并发程序设计算法,核心就是三个标志位是怎样控制两个方法对临界区的...
  • 直接附上安装包百度云链接直接先安装.NET安装包然后直接安装PAT软件即可 链接:https://pan.baidu.com/s/1L7AsNodFer7tc1Qk-sDk0g 提取码:dcj3 另附官网网址https://pat.comp.nus.edu.sg/ ...
  • 今天我们来看看2PC协议,不知道大家对2PC协议是不是了解,我们先简单介绍一下。 两阶段提交协议(two phase commit protocol, 2PC)可以保证数据的强一致性,许多分布式关系型数据管理系统采用此协议来完成分布式...
  • NEITHER PROVED NOR DISPROVED),这里如果我们修改过来的人数,就可以看到验证结果是没有问题的。  接下来定义了变量,变量是写为真且读的个数大余0的取反,这个在每个状态都是对的,因为可以写的时候读的必须...
  • 1.对于在另一个文件中加载已经存在的文件来说,初学者一般都会遇到一个问题,就是:Unable to locate library yerenguohe. 这句话表示无法加载指定的文件,那么解决 方法是什么呢?其实非常简单,首先,要确保被...
  • 为提高下一代列车运行控制(简称列控)系统安全计算机的系统兼容性,首先对其结构进行简要分析,并对管理机制进行设计,建立了管理单元状态转移模型,同时以形式化验证工具对模型的正确性进行了验证。在此基础上对...
  • 操作系统形式化验证实践教程(4) - 工具环境 如前面我们所了解的,Isabelle/HOL是套相当复杂的系统,它的底层基于Standard ML语言,它自己使用HOL和Isar语言,它可以生成ocaml,haskell和scala的代码,它有要使用到很...
  • 用ATL语言来形式化描述公平交换协议,并使用ATS(Alternating Transition Systems,交替转移系统)来为公平交换协议进行形式化建模,再用形式化验证工具MOCHA对公平交换协议的公平性(Fairness)、及时性...
  • 操作系统形式化验证实践教程(3) - 自动证明工具 归纳推理的推广 在第一节,我们学习了自然性的归纳法推理。大家都学过数学归纳法,对此应该或清晰或模糊有个概念。 其实,大家打破思维限制,归纳推理其实可以应用在...
  • 摘要:IP验证传统上包括某种形式的受约束的随机验证方法,例如UVM,也可能包括对设计的一部分进行形式化验证。但是,在运行第一个随机测试之前,通常都有一个将所有验证基础架构汇总的提前期,并且覆盖率闭合也很...
  • modex,即model eXtractor,由bell实验室开发,基于spin的模型检测工具,modex通过自定义的test harness来从C源代码中抽取出需要验证的spin模型。然后调用spin进行处理,最后编译spin处理过的C代码,生成名为pan.exe...
  • web服务形式化验证

    2013-07-20 23:17:54
    web服务形式化验证,将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模...
  • 由我司自主开发的国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink是一款支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder支持同步数据流以及状态...
  • Web服务的形式化验证

    2021-02-23 11:59:11
    将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模,并验证该实例。实验...
  • 因此,笔者特地将着眼点聚焦于『形式化验证』,选取当前行业内主流的两大形式化验证工具 (VaaS & Mythril) ,进行了一个简单的测试对比。 特别指出,用以测试的Mythril工具版本为『0.21.12』。 以下为相关的测试...
  • 针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的...
  • 操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作。 那么能不能让这个模式化的工作自动化起来,...
  • 针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 688
精华内容 275
关键字:

形式化验证工具