• 2024年第35卷第9期文章目次
    全 选
    显示方式: |
    • 完备神经网络验证加速技术综述

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007127

      摘要 (188) HTML (0) PDF 3.00 M (508) 评论 (0) 收藏

      摘要:人工智能技术已被广泛应用于生活中的各个领域.然而,神经网络作为人工智能的主要实现手段,在面对训练数据之外的输入或对抗攻击时,可能表现出意料之外的行为.在自动驾驶、智能医疗等安全攸关领域,这些未定义行为可能会对生命安全造成重大威胁.因此,使用完备验证方法证明神经网络的性质,保障其行为的正确性显得尤为重要.为了提高验证效率,各种完备神经网络验证工具均提出各自的优化方法,但并未充分探索这些方法真正起到的作用,后来的研究者难以从中找出最有效的优化方向.本综述介绍了神经网络验证领域的通用技术,并提出一个完备神经网络验证的通用框架.在此框架中,我们重点讨论了目前最先进的工具在约束求解、分支选择与边界计算这三个核心部分上的所采用的优化方法.针对各个工具本身的性能和核心加速方法,我们设计了一系列实验,旨在探究各种加速方式对于工具性能的贡献,并尝试寻找最有效的加速策略和更具潜力的优化方向,为研究者提供有价值的参考.

    • 舰载机弹药保障作业调度的形式化建模与验证

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007128

      摘要 (158) HTML (0) PDF 871.46 K (509) 评论 (0) 收藏

      摘要:航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器Coq对作业规划方案进行形式化验证.首先提出一个符合弹药保障作业特征的序列化双层资源堆模型;基于该模型,构造一套可用于描述作业执行行为的建模语言及其操作语义;最后在Coq中实现一种证明辅助工具.通过几个典型弹药保障作业规划方案的交互式证明实例,验证工具的可用性与工程实用性.

    • 并发对象强可线性化性质的检测和验证研究

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007130

      摘要 (135) HTML (0) PDF 782.62 K (377) 评论 (0) 收藏

      摘要:可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准。为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性。关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性。对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见。

    • 基于DH标定的机器人正向运动学形式化验证

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007131

      摘要 (127) HTML (0) PDF 1.19 M (491) 评论 (0) 收藏

      摘要:DH坐标系在机器人运动学分析中发挥着重要的作用。在基于DH坐标系构建的机器人控制系统中,机器人结构的复杂性使得构建安全的控制系统成为一个难题,仅仅依靠人工方法可能导致系统漏洞和安全风险,从而危及机器人的安全。形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证。基于此,本文设计了基于DH标定的机器人正向运动学的形式化验证框架。在Coq中构建了机器人运动理论的形式化证明,并验证控制算法的正确性以确保机器人的运动安全。首先,对DH坐标系进行形式化建模,构建相邻坐标系间转换矩阵的形式化定义,并验证了该转换矩阵与复合螺旋运动的等价性;其次,构建了机械臂正向运动学的形式化定义,并对机械臂运动的可分解性进行形式化验证;再次,本文对工业机器人中常见连杆结构及机器人进行形式化建模,并完成了正向运动学的形式化验证;最后,本文实现了Coq到OCaml的代码抽取,并对抽取的代码进行分析与验证。

    • 命令式动态规划类算法程序推导及机械化验证

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007134

      摘要 (118) HTML (0) PDF 1.59 M (419) 评论 (0) 收藏

      摘要:动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.

    • Trie+结构函数式建模、机械化验证及其应用

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007135

      摘要 (147) HTML (0) PDF 3.66 M (384) 评论 (0) 收藏

      摘要:Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.T.Nipkow给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,本文基于索引即键值的思想提出的Trie+结构,相较于传统的索引与键值分开存储的结构能减少50%的存储空间,大大提高了空间利用率.并且,对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证,保证操作的正确性和可靠性.进一步,首次提出一种匹配算法的通用验证规约,旨在解决一系列的匹配算法正确性验证问题.最后,基于Trie+结构与匹配算法通用验证规约,建模和验证了函数式中英文混合多模式匹配算法,发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug.所提的Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中,有一定的理论和应用价值.

    • 基于MTRDL的自动飞行系统模式需求建模与验证方法[1]

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007136

      摘要 (131) HTML (0) PDF 1.09 M (432) 评论 (0) 收藏

      摘要:在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.本文工作提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL,和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明了本文方法在自动飞行系统模式转换需求验证中的有效性.

    • 基于AADL的混合关键系统随机错误与突发错误安全性分析

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007137

      摘要 (145) HTML (0) PDF 1.30 M (359) 评论 (0) 收藏

      摘要:许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system,简称MCS).MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,甚至导致系统故障.目前的研究仅集中于对MCS的可调度性分析,未能进一步分析系统安全性,未能考虑线程之间的依赖关系.本文以随机错误和突发错误为研究对象,提出一种集成故障传播分析的基于架构的MCS安全分析方法.使用架构分析和设计语言(Architecture Analysis and Design Language,简称AADL)刻画构件依赖关系.为了弥补AADL的不足,创建新的AADL属性(AADL突发错误属性),并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程.为了将概率模型检查应用于安全分析,提出模型转换规则和组装方法,从AADL模型推导出PRISM模型.建立了两个公式,分别获得定量安全属性以验证故障发生的概率,以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析.最后,以动力艇自动驾驶仪(power boat autopilot,简称PBA)系统为例,验证了该方法的有效性.

    • 基于交互式定理证明的并发程序验证工作综述

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007138

      摘要 (147) HTML (0) PDF 2.10 M (461) 评论 (0) 收藏

      摘要:并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。

    • Büchi自动机确定化分析工具

      2024, 35(9):0-0. DOI: 10.13328/j.cnki.jos.007139

      摘要 (144) HTML (0) PDF 1.25 M (378) 评论 (0) 收藏

      摘要:无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,我们希望重点研究确定化过程中的索引能否继续被优化的问题,实现了确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.

    • 微内核操作系统互斥量模块功能正确性的形式化验证

      2024, 35(9):1-14. DOI: 10.13328/j.cnki.jos.007132

      摘要 (125) HTML (0) PDF 6.92 M (434) 评论 (0) 收藏

      摘要:操作系统在许多安全攸关领域为软件系统提供关键性底层支撑, 操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障, 造成巨大经济损失或危及人身安全. 为了减少此类安全事故的发生, 对操作系统正确性进行验证十分必要. 传统测试手段无法穷尽系统中的所有潜在错误, 因而操作系统验证有必要使用具有严格数学理论基础的形式化方法. 在操作系统中, 互斥量可协调多任务对资源的访问, 是一种常用的任务同步方式, 其功能正确性对于保障多任务应用的正确性十分关键. 基于定理证明方法, 在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模, 给出其接口函数的形式化规范, 并实现这些接口函数的功能正确性验证.

    • 基于形式化方法的区块链系统漏洞检测模型

      2024, 35(9):1-25. DOI: 10.13328/j.cnki.jos.007133

      摘要 (247) HTML (0) PDF 7.00 M (633) 评论 (0) 收藏

      摘要:随着区块链技术在各行各业的广泛应用, 区块链系统的架构变得越来越复杂, 这也增加了安全问题的数量. 目前, 在区块链系统中采用了模糊测试、符号执行等传统的漏洞检测方法, 但这些技术无法有效检测出未知的漏洞. 为了提高区块链系统的安全性, 提出基于形式化方法的区块链系统漏洞检测模型VDMBS (vulnerability detection model for blockchain systems), 所提模型综合系统迁移状态、安全规约和节点间信任关系等多种安全因素, 同时提供基于业务流程执行语言BPEL (business process execution language)的漏洞模型构建方法. 最后, 用NuSMV在基于区块链的电子投票选举系统上验证所提出的漏洞检测模型的有效性, 实验结果表明, 与现有的5种形式化测试工具相比, 所提出的VDMBS模型能够检测出更多的区块链系统业务逻辑漏洞和智能合约漏洞.

    • 关于安全案例论证构建的综述

      2024, 35(9):1-25. DOI: 10.13328/j.cnki.jos.007126

      摘要 (185) HTML (0) PDF 7.42 M (506) 评论 (0) 收藏

      摘要:安全案例提供清晰、全面和可靠的论据, 说明系统在特定环境下的操作满足可接受的安全性. 在受监管的安全攸关领域, 如汽车、航空和核能等领域, 认证机构通常要求系统经过严格的安全评估程序, 以确保其符合一个或多个安全标准. 在系统开发中应用安全案例是一种新兴的技术手段, 以结构化和全面的方式表达安全攸关系统的安全属性. 对安全案例的4个基本构建步骤: 确定目标、收集证据、构建论证和评估安全案例, 进行简要介绍. 然后聚焦于构建论证这一关键步骤, 详细介绍现有的8种安全案例表达形式, 包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等, 并分析了它们的优缺点. 由于安全案例所需材料的显著复杂性, 软件工具通常被用作构建和评估安全案例的实用方法. 比较7种用于安全案例开发和评估的工具, 包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE. 此外, 还深入探讨了安全案例构建中所面临的多重挑战, 这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面. 最后, 展望安全案例的未来研究方向, 揭示其潜在应用和研究问题.

当期目录


文章目录

过刊浏览

年份

刊期

联系方式
  • 《软件学报 》
  • 主办单位:中国科学院软件研究所
                     中国计算机学会
  • 邮编:100190
  • 电话:010-62562563
  • 电子邮箱:jos@iscas.ac.cn
  • 网址:https://www.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号