首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到20条相似文献,搜索用时 79 毫秒
1.
安全协议的形式化方法概述   总被引:2,自引:0,他引:2  
介绍了安全协议的形式化分析思路,阐述了安全协议形式化描述、需求、验证及设计四个方面的研究状况和它们的基本原理,并对常用的几种形式化验证技术的优缺点进行了分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。  相似文献   

2.
闫倩倩  缪炜恺 《计算机工程》2021,47(8):284-293,300
针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供模板。在对需求的确认和验证中,根据形式化规范建立需求模型,导出相关图表,基于此检查领域专家关注的场景。同时制定场景描述规则,使场景可以在需求模型中正确执行。在此基础上,从特殊变量、效率、场景质量三方面对场景进行优化,更充分地验证需求的正确性。实验结果表明,对于典型车载控制软件,该方法较传统分析方法可多探测到10%的潜在缺陷,效率提升80%以上。  相似文献   

3.
模型检验是软件工程形式化方法的一个重要组成部分,线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法,该方法针对不带有不确定性的概率模型,运用统计模型检验的方法,基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。  相似文献   

4.
张慧  郑超美 《计算机安全》2007,(1):36-37,48
安全协议验证是网络安全领域中重大课题之一,目前对安全协议进行分析的主流方法是形式化方法。该文对现在常用的几种形式化验证方法进行了概述和分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。  相似文献   

5.
基于市场法及能力分类的多机器人任务分配方法   总被引:7,自引:0,他引:7  
柳林  季秀才  郑志强 《机器人》2006,28(3):337-343
针对多机器人系统研究中如何有效地实现复杂任务的分布式动态分配这个基础性问题,提出了一种对这类问题进行形式化描述的一般方法.该方法从能力分类的角度出发,提出了机器人及任务能力向量的概念,并对多机器人任务分配问题进行了形式化描述,讨论了单个及多个机器人合作完成任务的能力条件.基于这种形式化描述方法,提出了一种采用市场机制的完全分布式的多机器人任务分配方法.仿真实验结果表明该方法能够有效地实现多机器人复杂任务的动态分布式分配.  相似文献   

6.
基于UML的软件形式化需求分析与验证   总被引:1,自引:0,他引:1  
姚全珠  王江 《计算机工程》2010,36(13):30-33
针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言(UML)模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。  相似文献   

7.
秦楠  马亮  黄锐 《计算机应用》2005,40(11):3261-3266
针对传统系统理论过程分析(STPA)方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。  相似文献   

8.
一种基于BLP模型的安全Web服务器系统   总被引:7,自引:0,他引:7  
刘克龙  卿斯汉  冯登国 《计算机学报》2003,26(10):1280-1287
针对基于Web的通信存在的弱点,提出了安全Web服务器的概念,并以此为目标,提出并实现了一种基于BLP形式化模型的安全Web服务器系统.  相似文献   

9.
针对关系数据库语义表达的不足,讨论了一种语义数据模型--基于范畴论的素描数据模型,从素描数据模型的形式化定义出发,以一种非形式化的方法分析了素描数据模型的基本概念,为更好地使用素描数据模型提供了基础.  相似文献   

10.
在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方法的复杂度。  相似文献   

11.
A Formal Object Approach to the Design of ZML   总被引:2,自引:0,他引:2  
This paper addresses two issues: how formal object modeling techniques facilitate the XML application development and how XML technology helps formal/graphical software design process. In particular, the paper presents a XML/XSL approach to the development of a web environment for Z family languages (Z/Object-Z/TCOZ). The projection techniques and tools from object-oriented Z (in XML) to UML (in XMI) are developed using XSL Transformations (XSLT). Furthermore, object-oriented Z is used to specify and design the essential functionalities of the web environment and the projection tools to UML. In a sense, the paper also demonstrates a formal object approach to modeling XML applications.  相似文献   

12.
提出了XML的形式数据模型及其查询代数,主要包括以下几个方面:构造先后序关系、引入带根连通有向图、建立XML形式数据模型(XFDM)和XML查询代数(XFQA)。它形成了一个较为完整的XML数据库管理系统的理论基础,可以作为XML以及其它半结构化数据库管理系统查询存储、查询分解、查询优化和查询实现的形式化基础。  相似文献   

13.
用形式方法开发软件可提高软件系统的正确性和可靠性,并可提高软件开发的效率。Z是一种基于状态的形式规格说明语言。但是一直以来形式方法在工业上不能得到普遍的应用,一个原因是它缺乏有效的支持工具以及向通用的工业标准转化的连接。本文首先用JAVA语言和XML开发了一种方法,使得用户能够在不同的平台上、不同的浏览器上利用GUI的方式编辑Z规格说明,进而转化成服务器端的以XML方式描述的Z模式。通过XSL所定义的格式,又将以XML方式描述的Z发布到网页上。从而实现了Z规格说明在WWW环境下的共享与发布。  相似文献   

14.
利用形式化模型的形式简洁、描述清晰、逻辑性强、易于扩展以及实用性强等优点,运用基于类型理论的逻辑化形式建模技术对XML,类型系统进行了形式化建模,实现了对各种XML数据的类型定义和对.XML擞据处理过程的类型检验,为可直接存储和检索XML数据的XML擞据库DM4提供了一种有效的类型系统设计方案。  相似文献   

15.
Information imprecision and uncertainty exist in many real-world applications and for this reason fuzzy data modeling has been extensively investigated in various data models. Currently, huge amounts of electronic data are available on the Internet, and XML has been the de facto standard of information representation and exchange over the Web. This paper focuses on fuzzy XML data modeling, which is mainly involved in the representation model of the fuzzy XML, its conceptual design, and its storage in databases. Based on “possibility distribution theory”, we developed this fuzzy XML data model. We developed this fuzzy UML data model to design the fuzzy XML model conceptually. We investigated the formal conversions from the fuzzy UML model to the fuzzy XML model and the formal mapping from the fuzzy XML model to the fuzzy relational databases.  相似文献   

16.
XML强闭包依赖的研究   总被引:5,自引:2,他引:3  
殷丽凤  郝忠孝 《计算机科学》2008,35(11):195-198
XML闭包依赖是基本的完整性约束。当XML文档出现不完全信息时,XML闭包依赖同样对于阻止XML数据的更新异常、查询优化以及索引设计具有重要的意义。提出了在不完全信息环境下基于一致路径集合的XML强函数依赖和XML强闭包依赖的定义,研究了XML强闭包依赖的判定定理。在提出XML强闭包依赖推理规则的基础上,对其有效性和完备性进行了证明。最后分析了XML强闭包依赖和XML强函数依赖的关系。  相似文献   

17.
XML is becoming a prevalent format and standard for data exchange in many applications. With the increase of XML data, there is an urgent need to research some efficient methods to store and manage XML data. As relational databases are the primary choices for this purpose considering their data management power, it is necessary to research the problem of mapping XML schemas to relational schemas. The semantics of XML schemas are crucial to design, query, and store XML documents and functional dependencies are very important representations of semantic information of XML schemas. As DTDs are one of the most frequently used schemas for XML documents in these days, we will use DTDs as schemas of XML documents here. This paper proposes the concept and the formal definition of XML functional dependencies over DTDs. A method to map XML DTDs to relational schemas with constraints such as functional dependencies, domain constraints, choice constraints, reference constraints, and cardinality constraints over DTDs is given, which can preserve the structures of DTDs as well as the semantics implied by the above constraints over DTDs. The concepts and method of mapping DTDs to relational schemas presented in the paper can be extended to the field of XML Schema just with some modifications in related formal definitions.  相似文献   

18.
基于XML的SQL Server数据库技能操作自动阅卷   总被引:2,自引:2,他引:0       下载免费PDF全文
针对SQL Server数据库技能测评系统缺乏的现状,分析了现有逻辑形式化自动阅卷技术,提出了基于XML实现SQL Server数据库技能操作自动阅卷方案。介绍了自动阅卷的实现原理和流程,重点阐述了两个关键技术环节:XML形式化表达和XML形式化自动阅卷技术。阅卷效果表明,基于XML的SQL Server数据库技能操作自动阅卷是切实可行的。  相似文献   

19.
范书义  王成  姜会霞 《测控技术》2013,32(2):104-109
自动测试描述语言(ATML)用于对ATS相关测试信息的标准化描述,这些信息以XML格式表示,其中包含对测试流程的描述.在自动生成测试程序过程中,需要采用编译技术将ATML文档转换为测试程序,要求输入的文件必须采用形式化描述,因此需要将XML格式表示的测试流程信息转换为形式化描述.在研究ATML中测试流程信息结构和实际含义基础上,设计了表示测试流程信息的形式化描述语言.实践表明,该形式化描述语言可以实现测试流程信息的形式化描述,满足测试程序自动生成的要求.  相似文献   

20.
XQuery语言用于查询XML文档。目前,该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化,本文通过重用XML家族语言通用语义构件的方法,形式化建模XQuery语言的语义,语义的描述采用Object—Z规范语言。这种面向对象的语义描述不仅具有简洁性、可扩展性和可组合性,而且有助于规范之间的一致性和协调性。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号