形式化方法

摘要： 在核安全级DCS平台和睦系统中,安全控制显示装置提供基于VDU技术的设备操作(如专设安全设施等)及电站安全参数监视显示功能。安全控制显示装置是一种满足核安全级A类要求的数字化显示装置,安全控制显示装置显示的图形画面一般由图形组态软件生成。图形组态软件通常只能运行于Windows操作系统中,不能运行于国产操作系统中,这也成为核安全级DCS国产化的瓶颈。因此,提出的一种可运行于国产操作系统的基于WEB技术图形组态软件技术方案不仅能满足图形软件国产化的要求,同时生成的图形应用软件还可以满足核安全级显示设备的要求。除核安全级DCS外,该技术还可应用于航空、航天、高铁等高安全领域,应用前景非常广阔。

摘要： 现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准,使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战.工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析,包括:ART工具平台所采用的变量关系(VRM)理论模型、平台架构和平台工具链,基于多范式的需求一致性、完整性形式化分析方法,EICAS系统的条目化初始自然语言需求的形式化建模和需求模型的自动化分析过程,如:需求条目的预处理、规范化处理、需求模型自动生成以及多范式分析等;给出了工程需求实例研究的经验总结和思考.

摘要： 针对可重构分布式综合模块化航空电子(distributed integrated modular avionics,DIMA)系统在设计初期缺少仿真与验证手段的问题,首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system management,GSM)的组件功能划分。然后,使用架构分析与设计语言(architecture analysis and design language,AADL)及其相关附件对DIMA动态重构的架构基础、行为细节等要素进行建模。在此基础上,设计了一种基于形式化定义的模型转换规则,该规则将AADL动态重构模型转换成可执行的时间自动机模型。最后,利用模型验证工具UPPAAL验证了可重构DIMA系统逻辑及时序的正确性和不安全控制行为的可达性。结果表明,所提方法具有可行性和有效性,并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

摘要： 为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

摘要： 随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.

摘要： 联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分。传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路。考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突。为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法。通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型。为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达。以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验。在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验。研究结果表明:模型的行为特性同子系统预期相一致,能够正确表达系统的行为。所设计子系统满足功能安全需求,可为底层实现提供依据。

摘要： 增强飞行视景系统(EFVS)作为机载复杂电子系统,其常规失效分析复杂易出错。基于此,引入形式化建模概念,提出了一种基于故障耦合模型的EFVS形式化建模方法。通过EFVS功能交互模型,明确系统失效传播模式;对该系统的架构和数据流进行抽象,分层建立该系统的故障耦合形式化模型;引入模型检验工具对系统模型进行验证,并结合典型的系统失效状态进行自动化运算,获取该失效状态的故障树最小割集。结果表明,所提方法自动化程度高,有助于提高EFVS失效分析过程的效率。

摘要： 随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.

摘要： 分析目前计算机和软件工程专业形式化方法类课程的现状,并根据软件工程发展形势的最新要求以及课程体系与ACM/IEEE CS2013计算机科学课程体系规范中知识主体的对应关系,指出现行课程体系的可改进之处,阐述重新构建形式化方法类课程体系的可行途径.

摘要： 形式化方法基于严格的数学方法规约、设计、构建、验证、演进计算系统,是改善和保障计算系统可信性的重要方法.形式化方法相关基础理论、技术和工具已成功应用于各种软硬件系统的设计与验证.近年来,在区块链、深度学习、量子计算等新兴领域,形式化方法也逐步应用适配,提升新兴领域计算系统的可信性.

摘要： 本文在介绍形式化方法和统一系统概括、模型的基础上,比较了常规方法和形式化方法,探讨了形式化方法在统一系统中各个阶段的规范应用,以及需求建模,得出了形式化方法所具有的特点有助于系统的实现和完善,同时使用petri网模型验证了统一系统中案件办理流程的路由结构.

摘要： 企业内控信息化实施是指通过信息技术手段将内控理念、内部控制制度规范、流程、控制措施固化到信息系统中,建立一个集成了企业内控需求的管理信息系统.企业内控信息化实施是一个复杂庞大的系统工程,需要有科学规范的方法、工具和技术手段保证内控系统实施的质量.领域分析和形式化方法是计算机软件工程中对软硬件系统进行分析、规范、建模、证明的方法和技术,将其应用于企业内控信息化实施,可以在内控系统运行前,通过基于数理逻辑证明的方法快速有效的发现系统设计和实施中存在的缺陷漏洞,降低企业内控系统低效或失效的风险.本文以销售业务为例讨论了领域分析与形式化建模方法的内控信息化实施过程.

摘要： 形式化方法的研究与应用对提高航天器系统的可靠性具有重要作用,本文通过对航天器测试业务特点的分析,发现航天器测试业务可以由自动机理论模型来表示,因此对航天器测试业务建立一个自动机模型是可行的,并利用一个小的实例进行了举例说明.该方法的研究可应用于航天器测试用例的设计、自诊断分析和测试覆盖性分析等领域,是航天器系统可靠性设计与验证领域中的一种新的思路与方法.

摘要： SaaS(Software as a Service)伴随云计算而出现,它与传统软件有很大区别.本文根据SaaS软件的特点,提出支持SaaS软件成熟度的SaaS软件分层元模型,使用形式化方法对每一层进行建模描述.受到面向对象Petri网(OOPN)和有色Petri网(CPN)思想的启发,提出面向服务网结构SOP(Service-Oriented Petri Nets)和CSOP(Colored Service-Oriented Petri Nets).一方面,使用封装的库所元素代表服务,体现了服务对外的不可见,内部结构影响运行.另一方面,不同的颜色集代表不同租户请求,突出SaaS多租户的特点.这不仅为复杂的SaaS软件建模提供万法,还折叠系统变迁,压缩状态空间.最后,以一个CRM(Customer Relationship Management客户关系管理)SaaS软件系统为例,验证了本文工作的可行性.

摘要： 连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.

摘要： 本文介绍了城市轨道交通自主化信号系统的创新原动力是员工持股与组织架构，采用一种新的商业模式为信号BT模式，采用形式化方法对技术路线进行创新，具备自主创新能力的信号企业是协同创新的中心，为了最终交付出安全载客的系统，信号企业离不开政府、运营公司、高校研究院、生产企业这四条生命线。

摘要： 形式化方法是构建可信软件的重要途径.Koch曲线是典型的分形图形,本文使用形式化方法PAR及循环不变式开发策略,开发了基于L系统的Koch曲线非递归算法,并对其进行了形式化的正确性证明.直接面向非递归算法,在得到求解基于L系统的Koch曲线算法的循环不变式的同时,直接得到易读、高效且可靠的非递归算法.对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨.

摘要： 选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑——安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究.首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案.为了更好地描述改进协议,用SPALL系统对其安全属性进行了形式化描述,并做出安全分析.分析结果表明,改进协议能够确保密钥分发的正确性,并具有密钥机密性和强认证性,还能满足通信双方验证会话密钥一致性的要求.

摘要： 选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑——安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究.首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案.为了更好地描述改进协议,用SPALL系统对其安全属性进行了形式化描述,并做出安全分析.分析结果表明,改进协议能够确保密钥分发的正确性,并具有密钥机密性和强认证性,还能满足通信双方验证会话密钥一致性的要求.

摘要： 选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑——安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究.首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案.为了更好地描述改进协议,用SPALL系统对其安全属性进行了形式化描述,并做出安全分析.分析结果表明,改进协议能够确保密钥分发的正确性,并具有密钥机密性和强认证性,还能满足通信双方验证会话密钥一致性的要求.

摘要： 本发明公开了一种基于形式化转换规则的航电领域需求的规范化方法，包括：S1，定义自然语言需求语句中的语句组成结构；S2，制定原始自然语言需求到规范化需求的转换规则；S3，利用Stanford Parser词法分析器得到原始自然语言需求语句相应的抽象语法树，从原始自然语言需求当中提取规范化需求需要的语句结构内容将其存入集合，再从集合中提取相应的语句结构内容并按照步骤S2中的转换规则进行输出，得到对应的规范化需求。本发明成功解决了传统自然语言需求语句中出现的歧义、模糊、不可验证等问题，对航空电子显控系统进行正确的需求分析。

摘要： 本发明公开了一种基于形式化方法的内生安全应用软件形式建模方法，所述建模部分包括如下部分：应用软件功能建模，以支持对系统功能进行描述，包括系统结构建模和系统行为建模两部分。系统结构建模是对系统架构建模，使用类图对系统中所涉及的属性和方法进行描述，系统行为建模采用状态图和序列图对整个系统的行为进行建模，其中状态图描述进程的控制逻辑，序列图描述进程之间的交互过程；应用软件信息安全威胁和策略建模，以支持对系统安全威胁和安全策略进行描述。信息安全威胁建模使用攻击树来对系统各个模块在各个方面的脆弱性关联起来进行深入地分析，发现威胁网络安全的攻击路径并以树的方式呈现出来。

摘要： 本发明公开了一种基于形式化方法的物流运输无人车多任务规划方法，包括以下步骤：1)将无人车运行时所处的实际环境抽象成无人车可以识别的抽象迁移系统模型；2)将无人车需要完成的多个任务描述成一个形式化公式；3)将描述物流运输无人车任务的形式化公式转换成形式化自动机，然后将形式化自动机映射到抽象迁移系统模型中，生成可行策略域；4)用最优策略搜索算法，在所述可行策略域中搜索出最优任务执行策略映；5)将最优任务执行策略映射回抽象迁移系统，得到无人车在抽象迁移系统的最优路径。本发明通过对无人车的多个任务的完成顺序和路径进行规划和安排，使其完成所有任务的代价最小，从而为无人车提供完成多任务的最优策略。

摘要： 一种基于形式化方法的安全策略验证系统及方法，系统由策略验证和发布中心、终端设备和数据库服务器组成。方法为：策略验证和发布中心的信息收集模块从终端设备提取信息，漏洞检测与修复模块进行漏洞检测与修复，策略形式化模块生成安全策略，策略一致性验证模块对安全策略进行冲突检测和消除，策略完备性验证模块对安全策略进行完备性验证和修复，策略比较模块将当前终端设备上运行的安全策略与管理员期望的配置进行比较，策略配置模块将安全策略转换成终端设备能识别的命令，发给终端设备执行。本发明对网络安全策略的验证具有通用性、完整性、易用性和自动化的优点。

摘要： 本发明涉及一种用于电力系统规程知识的形式化方法及其形式化系统，形式化方法包括下述步骤：A、对知识形式化进行建模；B、对知识形式化进行描述。步骤A包括下述步骤：（1）确定基本概念及概念结构；（2）抽象出概念属性；（3）确定复杂概念；步骤B包括下述步骤：（4）提取规程中包含的规则；（5）使用形式化规则语言描述规则；（6）使用形式化语言描述基础知识。形式化系统包括知识形式化建模模块和知识形式化描述模块。本发明从各类规程文本中识别有效知识，并借助合理的知识形式化方法，将蕴含其中的知识转为可被系统分析和识别的显性知识，大大提高电力系统的运行效率和电网的整体智能化水平。

摘要： 本发明公开了一种基于形式化方法内生安全应用软件形式建模方法，所述建模部分包括如下部分：应用软件功能建模，以支持对系统功能进行描述，包括系统结构建模和系统行为建模两部分。系统结构建模是对系统架构建模，使用类图对系统中所涉及的属性和方法进行描述，系统行为建模采用状态图和序列图对整个系统的行为进行建模，其中状态图描述进程的控制逻辑，序列图描述进程之间的交互过程；应用软件信息安全威胁和策略建模，以支持对系统安全威胁和安全策略进行描述。信息安全威胁建模使用攻击树来对系统各个模块在各个方面的脆弱性关联起来进行深入地分析，发现威胁网络安全的攻击路径并以树的方式呈现出来。

摘要： 本发明公开了一种结合形式化方法的智能配电网故障定位与恢复方法，包括以下步骤：1）分区域处理，将配电网划分为有源主干和无源支路，通过形式化方法验证分区域可靠性；2）解空间降维，生成联络环矩阵并重构配电网编码，剔除无效解，通过形式化方法验证降维合理性；3）故障信息转换，根据开关函数将线路故障信息转化为开关故障电流信息；4）通过启发式算法寻优，建立初始解库，根据目标函数进行全局快速寻优，通过形式化方法验证算法逻辑正确性；5）进行配电网故障阶段式恢复。将形式化方法运用在配电网故障定位和故障恢复方法中，对方法中关键特性和过程进行形式化验证，从根本上确保了方法的合理有效。

摘要： 本发明公开了一种基于形式化方法的物流运输无人车多任务规划方法，包括以下步骤：1)将无人车运行时所处的实际环境抽象成无人车可以识别的抽象迁移系统模型；2)将无人车需要完成的多个任务描述成一个形式化公式；3)将描述物流运输无人车任务的形式化公式转换成形式化自动机，然后将形式化自动机映射到抽象迁移系统模型中，生成可行策略域；4)用最优策略搜索算法，在所述可行策略域中搜索出最优任务执行策略映；5)将最优任务执行策略映射回抽象迁移系统，得到无人车在抽象迁移系统的最优路径。本发明通过对无人车的多个任务的完成顺序和路径进行规划和安排，使其完成所有任务的代价最小，从而为无人车提供完成多任务的最优策略。

摘要： 一种基于形式化方法的安全策略验证系统及方法，系统由策略验证和发布中心、终端设备和数据库服务器组成。方法为：策略验证和发布中心的信息收集模块从终端设备提取信息，漏洞检测与修复模块进行漏洞检测与修复，策略形式化模块生成安全策略，策略一致性验证模块对安全策略进行冲突检测和消除，策略完备性验证模块对安全策略进行完备性验证和修复，策略比较模块将当前终端设备上运行的安全策略与管理员期望的配置进行比较，策略配置模块将安全策略转换成终端设备能识别的命令，发给终端设备执行。本发明对网络安全策略的验证具有通用性、完整性、易用性和自动化的优点。

摘要： 本发明公开了一种基于形式化方法的ST语言编译器测试工具，该工具通过形式化方法为ST语言的执行制定了基准，不仅可以指导ST编译器的测试和实现，还可以为ST程序本身的分析提供支持。该测试工具包括四个部分：ST语言的形式化定义模块、程序模糊测试模块、程序变异模块以及编译器测试模块。该工具基于IEC 61131‑6标准以及多家厂商对ST语言的具体实现梳理ST语言的关键组成，形式化地制定相应的语法和语义关系作为语言的基准，模拟ST语言的具体执行过程，然后对ST程序及其输入进行有效变异，并进一步调用编译器测试模块实现对编译器的有效测试。