• 2022年第33卷第8期文章目次
    全 选
    显示方式: |
    • >专刊文章
    • 面向SQLite3数据库API调用序列的并行运行时验证方法

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006596

      摘要 (368) HTML (0) PDF 1.34 M (490) 评论 (0) 收藏

      摘要:作为轻量级的高可靠嵌入式数据库, SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域, 其提供了丰富灵活API函数以支持用户快速实现项目构建.然而, 不正确的API函数调用序列会导致严重后果, 包括运行错误、内存泄露和程序崩溃等.为了高效准确地监控SQLite3数据库API函数的正确调用情况, 本文提出了基于多核系统的并行运行时验证方法.该方法首先分析API函数文档, 自动挖掘相关API调用序列规约描述, 辅助人工将其形式化表达为具有完全正则表达能力的命题投影时序逻辑公式; 然后在程序运行时, 采用多任务调度策略, 将程序执行产生的状态序列分割并对不同片段并行验证.实验结果表明, 该方法能够发现调用SQLite3数据库API函数的30个被验证C程序中, 违背API函数调用序列规约的达16个.另外, 与传统串行运行时验证方法的对比实验表明, 本文提出的并行运行时验证方法能够有效提高多核系统的验证效率.

    • 一种利用非确定规划的LTL合成方法

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006597

      摘要 (271) HTML (0) PDF 708.52 K (349) 评论 (0) 收藏

      摘要:LTL合成(Linear Temporal Logic synthesis)是程序合成(program synthesis)的一类重要子问题, 旨在自动构建一个控制器(controller), 且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说, 可以将LTL合成定义为二人博弈(two-player game)问题, 博弈的双方是环境和控制器, 该问题的解称为合成策略.近年来, 有研究从理论角度讨论了LTL合成与非确定规划(non-deterministic planning)的相关性.基于此, 本文提出了一种新的利用非确定规划求解LTL合成问题的方法, 并证明了方法的正确性和完备性.具体而言, 首先获得LTL公式对应的Büchi自动机, 结合二人博弈定义, 将LTL合成问题转换为完全可观测的非确定规划模型, 然后交由高效规划器求解.通过实验结果说明, 与其他LTL合成方法相比, 本文提出的基于规划的合成方法在解质量方面具有较大的优势, 能够获得规模较小的合成策略.

    • 基于基本并行进程的异步通讯程序的验证方法与实现

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006598

      摘要 (235) HTML (0) PDF 1.01 M (373) 评论 (0) 收藏

      摘要:异步通讯程序是进程间通过异步消息通讯实现非阻塞并发的程序. 当前异步通讯程序的程序验证问题通常将其归约至向量加法系统及其扩展模型,因而复杂度很高,并缺乏高效工具. 基本并行进程作为向量加法系统的一个子类,其可达性的验证问题为NP完备.首先,本文改进了Osualdo等提出的为异步通讯程序建模的Actor通讯系统, 将其归约至基本并行进程. 然后,实现了基本并行进程的模型检测工具RABLE,实验结果表明,验证方法在异步通讯程序的一系列程序验证问题上具有比已有工具更高效的结果.

    • 运用时间分类树的确定单时钟时间自动机学习

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006599

      摘要 (203) HTML (0) PDF 1.72 M (249) 评论 (0) 收藏

      摘要:时间自动机的模型学习算法旨在通过提供输入和观察输出构建软硬件系统的形式化模型.确定性单时钟时间自动机的学习是其中的一个重要研究方向, 但是该算法具有一定的局限性, 在状态较多时学习速度较慢, 很难应用到复杂的系统中.由此, 我们提出了一种改进的学习算法, 使用逻辑时间分类树代替逻辑时间观察表作为学习算法的内部数据结构, 有效地减少了成员查询次数, 降低了算法的空间复杂度, 并能够高效率地构建假设自动机.最后我们进行了相关实验, 实验结果表明, 本文提出的改进算法减少了60%左右的成员查询和5%左右的等价查询.同时在该实验中, 改进算法的学习速度最高可提高45倍以上.

    • 面向CPS时空约束的资源建模及其安全性验证方法

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006600

      摘要 (373) HTML (0) PDF 1.52 M (453) 评论 (0) 收藏

      摘要:信息物理融合系统CPS(Cyber Physical System)是在环境感知的基础上,集合物理与计算的系统,可以实现与环境的智能交互.CPS信息物理空间的不断变化对CPS资源安全性造成一定的挑战.因此,如何研究这一类由时空变化而导致的CPS资源安全性问题成为关键.本文针对该问题提出了面向CPS时空约束的资源建模及其安全性验证方法.首先, 在TCSP(Timed Communicating Sequential Process)的基础上扩展资源向量,提出时空资源通信顺序进程DSR-TCSP(Duration-Space Resource TCSP),使其能够描述CPS拓扑环境下的资源;其次,从时空约束的资源安全性需求中获取时间安全需求,通过DSR-TCSP的时间属性验证算法对时间安全需求进行验证;再次,将满足时间安全需求的模型转换为偶图与偶图反应,并输入到偶图检验工具BigMC中,验证其物理拓扑安全需求,对没有通过验证的反例,修改DSR-TCSP模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.

    • 基于消息传递关系网络的布尔可满足性预测

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006601

      摘要 (236) HTML (0) PDF 640.63 K (311) 评论 (0) 收藏

      摘要:布尔可满足性求解能够验证的问题规模通常受限, 因此, 如何高精度地预测布尔可满足性问题的可满足性是一个重要研究问题, 也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构, 但是这种表征方法缺少了变量、子句之间的重要关系信息.在我们的方法中, 通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系, 并设计使用消息传递关系网络模型来捕获实例的关系信息, 提取了更多的结构特征.结果表明, 该模型在预测精度、泛化能力和资源需求等方面均优于现有模型, 对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练, 在大规模数据集上预测的平均预测精度达到了80.8%.同时, 该模型对随机生成的非均匀随机问题的预测精度达到99%, 这意味着它学习了预测可满足性的重要特征.此外, 模型预测所花费的时间随着问题规模的增大也只是呈线性增长. 总结而言, 本文基于关系消息传递网络提出了一个预测精度更高, 泛化能力更好的布尔可满足性预测方法.

    • 智能合约的时间约束模式及其形式化验证

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006603

      摘要 (403) HTML (0) PDF 1.16 M (374) 评论 (0) 收藏

      摘要:智能合约是一套以数字形式定义的承诺.通过智能合约可以大大减少协议制定的中间环节, 提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入, 智能合约的作用必然越来越突出, 智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视, 但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.本文通过分析典型智能合约, 对智能合约时间约束的不同表现形式进行梳理, 提炼出相应的时间约束模式并对其进行形式化; 定义Solidity智能合约到时间自动机的转换规则并实现其到实时模型检测工具UPPAAL入口模型的自动转换; 再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究, 结果表明本文所提炼模式的普遍性以及本文所提出形式化验证方案的可行性和有效性.

    • TSO内存模型下限界可线性化的可判定性研究

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006604

      摘要 (271) HTML (0) PDF 585.31 K (302) 评论 (0) 收藏

      摘要:TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order(简称TSO)内存模型下可线性化的三个变种。在本文中我们提出了?-限界TSO-to-TSO可线性化和?-限界TSO可线性化,考察了?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题。它们分别是这三种可线性化的限界版本,都使用?-扩展历史,这样的扩展历史对应的执行有着限界数目(不超过?个)的函数调用、函数返回、调用刷出和返回刷出动作。?-扩展历史对应执行中的写动作数目是不限界的,进而执行中使用的存储缓冲区的大小也是不限界的,对应的操作语义是无穷状态迁移系统,所以三个限界版本可线性化的验证问题是不平凡的。 我们将定义在并发数据结构与顺序规约之间的?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题归约到?-扩展历史集合之间的TSO-to-TSO可线性化问题,从而以统一的方式验证了TSO内存模型下可线性化的三个限界版本。验证方法的关键步骤是判定一个并发数据结构是否有一个特定的?-扩展历史。我们证明了这个问题是可判定的,证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题。本质上,这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas(compare-and-swap)动作。在TSO-to-TSO可线性化的定义中,一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态。为了模拟函数调用或函数返回动作对存储缓冲区的影响,我们在每个函数调用或函数返回动作之后立刻执行一个特定的写动作。这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响。我们引入观察者进程,为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作,以这种方式模拟了函数调用或函数返回动作对控制状态的影响。因此,我们证明了TSO内存模型下可线性化的这三个限界版本都是可判定的。我们进而证明了在TSO内存模型下判定可线性化的这三个限界版本的复杂度都在递归函数的Fast-Growing层级中。我们通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的三个限界版本可以互相归约得到这个结论。

    • 基于深度学习和反例制导的循环程序秩函数生成

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006605

      摘要 (280) HTML (0) PDF 624.87 K (319) 评论 (0) 收藏

      摘要:程序终止性判定是程序分析与验证领域中的一个研究热点. 针对非线性循环程序, 提出了一种基于反例制导的神经网络型秩函数的构造方法. 该方法采用学习组件和验证组件交互的迭代框架, 其中学习组件利用程序轨迹作为训练集合构造一个候选秩函数, 验证组件运用可满足性模理论(Satisfiability Modulo Theories, SMT)确保候选秩函数的有效性, 而由SMT返回的反例则进一步用于扩展学习组件中的训练集合以对候选秩函数进行精化.实验结果表明, 所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.

    • 基于正时态测试器的实时分支时态逻辑符号化模型检测

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006606

      摘要 (265) HTML (0) PDF 1.29 M (313) 评论 (0) 收藏

      摘要:基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.

    • 模拟多核多任务实时系统的点区间优先级时间Petri网与TCTL模型检测

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006607

      摘要 (291) HTML (0) PDF 962.28 K (329) 评论 (0) 收藏

      摘要:时间Petri网为实时系统提供了一种形式化的建模方法, 时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式, 因此基于时间Petri网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统, 例如多核多任务实时系统, 这里不仅需要考虑任务之间的时间约束还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题, 致使相应的建模和分析变得更加困难.为此, 本文提出了点区间优先级时间Petri网, 通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性, 从而可以模拟实时系统的抢占式调度机制, 即首先高优先级的任务抢占低优先级的任务所占用的资源, 导致后者被中断, 然后前者执行完毕后释放资源, 最后后者再次获得资源从中断的地方恢复.本文通过点区间优先级时间Petri网来模拟多核多任务实时系统, 使用TCTL来描述它们的设计需求, 设计了相应的模型检测算法, 开发了相应的模型检测器以验证它们的正确性.我们通过一个实例来说明我们的模型和方法的有效性.

    • 一种面向抽象解释框架的函数内联过程间分析的优化方法

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006608

      摘要 (456) HTML (0) PDF 633.02 K (309) 评论 (0) 收藏

      摘要:分析实际程序时往往需要分析程序中函数的调用, 一般使用过程间分析来实现全程序分析.函数内联是一种最为精确、易于实现的过程间分析方法.通过函数内联, 可以使得已有过程内分析方法和工具支持包含函数调用的程序的分析.但是, 函数内联后代码的规模急剧增加, 同时将产生大量中间变量, 增加程序分析的变量维度, 导致程序分析过程时空开销大大增加.本文考虑基于抽象解释框架下函数内联过程间分析的一些不足, 并提出相应优化方法.基于抽象解释的程序分析关注自动推导程序变量之间的不变式约束关系, 因此程序变量构成的程序环境大小(即各程序点处须考虑的相关变量集合)对分析的时空开销具有重要影响.为了减少函数内联后程序分析的开销, 本文提出了面向内联函数块的程序环境降维优化方法.该方法针对内联函数后的程序代码, 分析确定不同程序点处需维护的程序环境(即相关变量集合), 而不是所有程序点共享同一全局程序环境, 从而实现程序状态的降维.详细描述了基于该方法所实现的工具DRIP (Dimension Reduction for analyzing function Inlined Program) 的架构、模块及算法细节.并在WCET Benchmarks测试集开展了分析实验, 实验结果表明: DRIP在变量消除上取得的效果良好, 甚至在某些测试集上能减少一半以上的变量, 并在一定程度上降低了分析过程的时空开销.

    • 基于锁耦合遍历算法的文件系统终止性验证

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006609

      摘要 (160) HTML (0) PDF 792.13 K (122) 评论 (0) 收藏

      摘要:并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.本文证明了一个并发文件系统AtomFS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明AtomFS接口的终止性要说明当其遇到阻碍时,阻碍源头(其它线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性,然而我们遇到了两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2)rename接口由于需要遍历两条路径,会带来”跨路径阻碍”现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.本文提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.我们成功的构建了一个终止性证明框架CRL-T,并验证了AtomFS的终止性,所有的证明都在Coq中实现.

    • 软硬件综合AADL可靠性建模及分析方法

      2022, 33(8):0-0. DOI: 10.13328/j.cnki.jos.006610

      摘要 (344) HTML (0) PDF 1.12 M (345) 评论 (0) 收藏

      摘要:目前嵌入式系统广泛应用于航空电子、远程医疗、汽车电子等具有高可靠性要求的系统中。随着嵌入式系统的复杂度越来越高,为了保障系统的高可靠性需求,需要在系统开发的早期设计阶段对系统的可靠性进行分析评估,以提高系统的开发效率。嵌入式系统中软件、硬件功能的失效都会对系统可靠性产生影响,而AADL的可靠性模型缺乏对硬件构件错误的影响及传播机制进行刻画分析的能力。本文综合考虑软、硬件错误发生失效后对系统可靠性的影响,提出了一种面向系统架构级别的软硬件综合可靠性分析方法。该方法基于电子电路设计中事务级建模方法,扩展了AADL事务级错误模型的语法和语义,来支持AADL对硬件构件错误传播的硬件功能行为建模,在此基础上,利用AADL模型实例化机制实现对嵌入式系统可靠性建模,刻画了错误行为在硬件构件之间、软硬件构件之间的传播与影响。同时,定义了AADL硬件构件事务级错误模型到广义随机Petri网模型的映射规则,实现了系统软、硬件综合的可靠性行为仿真计算模型组合,支持嵌入式系统的软硬件综合可靠性分析。论文开发了软硬件综合可靠性建模与分析工具原型,并以某型飞机空气增压系统为例,在航空电子系统架构设计中进行尝试,验证了该方法在复杂嵌入式系统设计中进行软硬件综合可靠性分析的可行性与优越性。

当期目录


文章目录

过刊浏览

年份

刊期

联系方式
  • 《软件学报 》
  • 主办单位:中国科学院软件研究所
                     中国计算机学会
  • 邮编:100190
  • 电话:010-62562563
  • 电子邮箱:jos@iscas.ac.cn
  • 网址:http://jos.org.cn/
  • 刊号:ISSN 1000-9825
  •           CN 11-2560/TP
  • 国内定价:70元
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号