共查询到20条相似文献,搜索用时 79 毫秒
1.
安全协议的形式化方法概述 总被引:2,自引:0,他引:2
介绍了安全协议的形式化分析思路,阐述了安全协议形式化描述、需求、验证及设计四个方面的研究状况和它们的基本原理,并对常用的几种形式化验证技术的优缺点进行了分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。 相似文献
2.
针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供模板。在对需求的确认和验证中,根据形式化规范建立需求模型,导出相关图表,基于此检查领域专家关注的场景。同时制定场景描述规则,使场景可以在需求模型中正确执行。在此基础上,从特殊变量、效率、场景质量三方面对场景进行优化,更充分地验证需求的正确性。实验结果表明,对于典型车载控制软件,该方法较传统分析方法可多探测到10%的潜在缺陷,效率提升80%以上。 相似文献
3.
安杰 《数字社区&智能家居》2014,(30):7097-7099
模型检验是软件工程形式化方法的一个重要组成部分,线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法,该方法针对不带有不确定性的概率模型,运用统计模型检验的方法,基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。 相似文献
4.
安全协议验证是网络安全领域中重大课题之一,目前对安全协议进行分析的主流方法是形式化方法。该文对现在常用的几种形式化验证方法进行了概述和分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。 相似文献
5.
6.
基于UML的软件形式化需求分析与验证 总被引:1,自引:0,他引:1
针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言(UML)模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。 相似文献
7.
针对传统系统理论过程分析(STPA)方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。 相似文献
8.
9.
针对关系数据库语义表达的不足,讨论了一种语义数据模型--基于范畴论的素描数据模型,从素描数据模型的形式化定义出发,以一种非形式化的方法分析了素描数据模型的基本概念,为更好地使用素描数据模型提供了基础. 相似文献
10.
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.
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
XML闭包依赖是基本的完整性约束。当XML文档出现不完全信息时,XML闭包依赖同样对于阻止XML数据的更新异常、查询优化以及索引设计具有重要的意义。提出了在不完全信息环境下基于一致路径集合的XML强函数依赖和XML强闭包依赖的定义,研究了XML强闭包依赖的判定定理。在提出XML强闭包依赖推理规则的基础上,对其有效性和完备性进行了证明。最后分析了XML强闭包依赖和XML强函数依赖的关系。 相似文献
17.
《Information and Software Technology》2006,48(4):245-252
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.
19.
20.
XQuery语言用于查询XML文档。目前,该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化,本文通过重用XML家族语言通用语义构件的方法,形式化建模XQuery语言的语义,语义的描述采用Object—Z规范语言。这种面向对象的语义描述不仅具有简洁性、可扩展性和可组合性,而且有助于规范之间的一致性和协调性。 相似文献