面向自然语言需求的验证性质生成方法  

Verification Properties Generation from Natural Language Requirements

作　　者：李晓劼 杨志斌[1,2] 王翰丰 周勇 李维[3] LI Xiaojie;YANG Zhibin;WANG Hanfeng;ZHOU Yong;LI Wei(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China;Aerospace Life-support Industries Ltd.,Xiangyang 441003,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统的软件开发与验证技术工信部重点实验室,南京211106 [3]航宇救生装备有限公司,襄阳441003

出　　处：《小型微型计算机系统》2024年第1期84-92,共9页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(62072233)资助;国防基础科研项目(JCKY2020205C006)资助;航空科学基金项目(201919052002)资助.

摘　　要：安全关键系统和软件的安全性、可靠性需要形式化验证来保障,使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约,这已成为当前形式化验证领域研究的热点和难点.当前的形式化规约提取工作大多针对英文需求,较少针对中文自然语言需求.此外,由于AADL具有强大的表达能力和完善的验证机制,已成为航空航天领域的主要建模语言之一,而现有的工作较少考虑如何从需求中提取AADL模型的验证性质.为了解决上述问题,本文提出一种面向自然语言需求的AADL模型验证性质自动生成方法,从自然语言需求中提取验证的相关性质,并将其转化为AADL模型验证工具AGREE可识别的形式化规约.首先,定义了模式定义语言(Contract Pattern Language,CPL),将需求划分为不同模式,并给出由固定句型和占位符组成的需求模板;其次,通过自然语言处理技术解析需求文本,获取替换需求模板中占位符的原子命题,以便生成完整的形式化规约;最后,设计并实现了相关工具,并将其用于工业界实际案例来说明该方法的可用性和有效性.The safety and reliability of safety-critical systems and software need to be guaranteed by formal verification,and the premise of using formal verification is to extract the relevant verification properties from the natural language requirements texts and transform them into formal specification,which has become a hot spot and difficulty in the field of formal verification.Most formal specification extraction work is aimed at English requirements and less for Chinese.In addition,AADL has become one of the main modeling languages in the aerospace field due to its strong expressive capabilities and perfect verification properties,while existing work has less consideration for how to extract the verification properties of AADL models.In order to solve these problems,this paper proposes an automatic generation method of AADL model verification properties based on natural language requirements,which extracts the properties of verification from natural language requirements,and transforms them into formal specifications recognizable by AGREE,the AADL model verification tool.Firstly,the Contract Pattern Language(CPL)is defined,which divides the requirements into different patterns and gives the requirements template composed of fixed sentence patterns and placeholders;Secondly,the requirements text is parsed by natural language processing technology,and the atomic propositions of the placeholders in the requirement templates are replaced in order to generate a complete formal specification;Finally,the relevant tools are designed and implemented,and they are used in industrial practical cases to illustrate the availability and effectiveness of the method.

关 键 词：形式化验证 模式定义语言 自然语言处理 规约生成 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]