一个高效的语法分析器生成工具

VPGE(Visual Parser Generation Environment)是一个可视化语法分析器集成开发环境,除了具有良好的界面和强大的调试功能,其LALR(1)分析器的生成速度达到并超过公认的分析器生成速度最快的LALR(1)分析器自动生成器Bison,所能处理的文法规模也优于Bison.本文在DeRemer和Pennello的LALR(1)分析器自动生成基本原理的基础上,在设计数据结构和算法实现中采用了大量优化技术.     

一个高效的语法分析器生成工具

VPGE(VisualParserGenerationEnvironment)是一个可视化语法分析器集成开发环境,除了具有良好的界面和强大的调试功能,其LALR(1)分析器的生成速度达到并超过公认的分析器生成速度最快的LALR(1)分析器自动生成器Bison,所能处理的文法规模也优于Bison.本文在DeRemer和Pen-nello的LALR(1)分析器自动生成基本原理的基础上,在设计数据结构和算法实现中采用了大量优化技术.     

同步数据流语言可信编译器Vélus与L2C的比较

同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注.近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器.同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.     

基于Z规格的LR(k)形式化分析及验证

在编译器的构造中,常由于语义的二义性等问题导致不正确的目标程序.为解决此问题,提出了一种新型的语法及语义正确性验证方案,即建立LR (k)文法和Z规格说明的联系,以此构造LR (k)文法的形式化描述及其形式化验证.实验结果表明,该方案能有效描述并检测LR (k)文法分析器中的语法错误及语义二义性,有助于提高分析器的有效性.     

LALR(1)语法分析器的自动生成

文章简单介绍了语法分析器自动生成的原理和技术，根据语法分析器的生成过程，介绍了实用的语法分析器的自动生成器各个部件及其实现的详细过程。     

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

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

微内核中断机制的形式化设计与验证

操作系统的正确性和安全性很难用定量的方法进行描述。形式化方法是操作系统设计和验证领域公认的标 准方法。以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证, 在自行开发的安全可信操作系统VTOS上加以实现,采用Isabelle/HOL对设计过程进行了形式化描述,对VTOS中 断机制的完整性进行了验证,这对操作系统的形式化设计和验证工作起到了一定的借鉴意义。     

静态程序分析过程中形式化验证工具Frama-C的应用

软件的静态程序分析是确保软件安全可靠的一种有效手段。常见的形式化的静态分析工具一般是基于模型检测,定理证明或抽象解释理论来对软件进行分析验证。然而,基于单一理论的验证工具具有一定的局限性。介绍了一个开源的静态分析平台Frama-C,根据该工具的特点,分别使用不同的插件对一小段代码进行静态分析,有助于将不同的程序分析方法相结合。最后对如何使用Frama-C工具解决航空控制软件等安全关键软件的执行时间分析问题的过程进行了演示。     

可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好”误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器,它以扩展的Lustre语言为源语言,以Clight （CompCert中的C语言子集）为目标语言.就我们所知,L2C是同类工作中唯一面向实际工业应用的同步数据流语言编译器.本文重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.     

基于Rebeca模型的硬件设计形式化验证

形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeca是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言,可以为不精通于形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeca的基础上,采用Rebeca对硬件设计进行建模,然后Modere形式化验证工具对AES密码芯片进行形式化验证。     

多旋翼飞控推进子系统的Coq形式化验证

飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.     

密码模块的形式化设计和验证研究

该文提出了运用形式化方法对密码模块进行辅助设计和验证的研究方向。首先介绍密码模块的相关知识和研究背景,给出了如何用形式化方法验证密码模块的过程,最后讨论在验证过程中可能存在的问题及解决方案。     

采用函数式语言的BPEL模型形式化验证方法

通信顺序进程(communicating sequential process,CSP)是一种经典的形式化方法,CSP_M是在CSP基础上提出的一种函数式语言。目前Web服务组合中BPEL(business process execution language)模型缺乏可执行的形式化编程语言,通过CSP_M提出了一种基于函数式语言的BPEL模型验证方法。首先给出了基于CSP_M的BPEL模型建模与验证框架;其次给出了CSP_M的进程代数定义;再次详细描述了BPEL语言到CSP以及CSP_M的映射方法;最后以一个在线购物系统为例,讨论了该方法的使用效果。实验表明该方法可以提高BPEL模型的可靠性。     

一种为二义性文法构造SLR(1)分析器的方法

文法具有二义性是实际中经常遇到的情况。本文以SLR（1）分析器为例介绍了一种为二义性文法构造语法分析器的方法,并通过实例分析了利用该方法进行语法分析的过程。     

微内核架构文件系统的形式化设计与验证方法研究

文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper-ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.     

ATLAS-C语法分析器中冲突消解问题的研究

论文对在设计ATLAS-C语法分析器中YACC工具所无法解决的冲突进行了具体的讨论与研究,并且对出现的冲突提出了相应的解决方案。实验结果证明论文提出的消解冲突的方法在设计语法分析器时具有可行性。     

安全数据库顶层规范中SQL操作的形式化分析与验证

介绍了安全数据库形式化顸层规范,定义了顶层规范中SQL操作的描述,在此基础上给出简单SQL操作的定义,并对其进行分析验证,最后将一般SQL操作的分析验证转换为多个简单SQL操作的分析验证.验证过程表明,该方法既对SQL操作作了完整清晰的描述,又简化了证明.     

面向需求的安全关键系统形式化建模与验证方法研究

在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML~(-e)语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML~(-e)模型转化成NuSMV 2模型的方法,并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。     

基于UML的作战仿真VV＆A过程形式化建模

可信性是作战仿真的生命线,对作战仿真的全生命周期进行校核、验证与确认（Verification,Validation and Accreditation,VV＆A）是确保其可信性的重要途径。建立合适的VV＆A过程形式化模型是开展作战仿真VV＆A过程研究的前提和基础。基于统一建模语言（Unified Modeling Language,UML）分别从用例、静态结构、动态行为及交互等方面对VV＆A过程进行形式化建模,建立了作战仿真VV＆A过程的用例、类图、活动图及顺序图模型,并给出相应的形式化定义。实践表明：作战仿真VV＆A过程形式化建模可以使VV＆A的描述规范化、标准化及形式化,便于不同领域人员的相互沟通与交流,以及VV＆A工程化应用,促进了VV＆A工作顺利开展。     

一种自然语言理解中语法分析的算法设计和实现

自然语言的理解是计算机研究的重要分支,主要体现在语法、语义和语音三方面.文章介绍了语法分析的各种方法,剖析了语言组成的结构关系,利用DELPHI语言编写了一种自顶向下的语法分析程序,并通过具体的实例验证了算法的正确性.