共查询到20条相似文献，搜索用时 282 毫秒
1.
本文详细分析了实时工作流中的时序约束。同时,为了对实时工作流时序约束进行形式化描述,本文利用时间自动机建模实时工作流的时序约束。这为实时工作流时序约束的形式化验证提供了基础。 相似文献
2.
3.
许柯 《中国科教创新导刊》2008,(26)
高效、可靠、全面的验证工作是可重用IP核开发成功的保证。本文针对可重用IP软核的验证过程进行研究,主要从RTL级功能验证、静态时序分析和RTL级与网表之间的形式化验证三个方面入手,研究了当前主流的验证方法,分析各种方法的优点和存在的缺陷,并给出了建议性的解决方法。 相似文献
4.
5.
软件开发中的形式化方法介绍 总被引：2，自引：0，他引：2
软件工程中的形式化方法就是依靠数学模型和计算来描述和验证一个目标软件系统的行为和特性,包括需求规格、设计和实现等,其最根本的一点就是建立在严格的数学基础上的方法.使用形式化方法可以帮助开发者获得对其所描述的系统的深刻而正确的理解,发现并及时更正设计中的错误和缺陷.众多的形式化方法在功能上可以实现互补.目前软件开发中的形式化方法主要是形式化规范说明语言,有Z语言、VDM语言和RAISE语言等. 相似文献
6.
7.
介绍了寄存器转换语言(RTL)3个组成部分的内容,包括RTL的对象类型、RTL的分类和格式以及如何访问其操作数,这些是学习RTL的基础。 相似文献
8.
描述逻辑是一族知识表示语言,其以结构化、形式化方法表示特定应用领域的知识。描述逻辑的各语言背后的逻辑是什么,能否公理化等问题在描述逻辑的研究进程中迄今没有相关研究。本文首先通过描述逻辑ALC与一阶逻辑的一个可判定片段之间的关系试图揭示描述逻辑的本质。最后给出了描述逻辑ALC的公理化方法及其演绎定理的证明。 相似文献
9.
基于OWL的网络管理领域本体构建方法 总被引：2，自引：0，他引：2
为了解决网络管理信息语义描述的问题,通过研究本体理论、OWL本体语言和描述逻辑,提出基于OWL语言的网络管理领域本体构建方法．领域专家首先获取网络管理领域已有知识,然后定义类、属性、实例以及公理并用OWL语言形式化本体．最后通过用Protege工具构建局域网部分本体的实验验证,结果表明该方法是可行的． 相似文献
10.
统一建模语言UML在面向对象的建模技术中得到了广泛应用。但是UML模型缺乏形式化语义,难以使用数学方式对模型进行分析和验证。B方法作为一种建立在严格数学机理上的形式化方法,将可视化UML模型转换为B形式化规范,可以对模型进行形式化描述和分析,确保模型的可靠性。通过研究从UML状态图到B形式规范的转换规则,提出了一种基于XMI的状态图到B形式化规范的自动转换方法,并使用Java语言实现了自动转换工具UML2B。 相似文献
11.
吕进 《西南师范大学学报(人文社会科学版)》2010,(2):70-74
命题时态逻辑PTL是一个可广泛应用于人工智能的逻辑,其特点是只有表达未来的时态算子。它刻画了人工智能研究中往往只需要描述未来状态,而不必关注过去的性质。PTL给出了一个表达时间具有向上线性、传递性、持续性和离散性的公理化逻辑系统,并证明了其可靠性和完全性。 相似文献
12.
成功设计一个复杂数字系统要求在设计的各个阶段验证实现的正确性,传统的模拟验证已不能完全满足需要,形式验证技术成为了重要的补充.研究了国内外形式验证技术的研究成果,对主要方法进行了分析和比较并对新的热点进行了展望. 相似文献
13.
怎样基于教育建模语言（Educational Modeling Language,简称EML）开展形式化层次的教学设计,是教学设计自动化领域中一个值得探讨的问题。IMSLD规范是一种经过改造的EML,具有目标、性质、基础、体系、提出者等五个方面的特点。基于IMSLD规范的学习（单元）设计有四条原理：指导思想原理、要素结构原理、设计层次原理、创设流程原理。从九个维度进一步对国际上已经推出的20多个IMSLD工具进行了归类和比较,并以《教育技术原理》教改课程为例,阐述了基于IMSLD规范的“学习单元”设计的具体过程,简介了“学习单元”设计制品的四条应用途径。 相似文献
14.
This paper describes a case study presented to students in computer science during a course on formal techniques for protocol validation. The course teaches some basic notions on specification, simulation, verification, testing and distributed observation. The case study is the classical alternating-bit protocol. The exercise first consists of some simple modeling and simulation of the specification and verification of some basic service properties. It is then followed with the problem of observation of distributed executions of the protocol. This kind of experiment was found to be useful for students, since they gain an understanding of the importance and necessity of formal methods for protocol validation. 相似文献
15.
为准确计算正三角形广告牌面板上的风荷载,对比了《户外广告设施钢结构技术规程》（CECS148：2003）和《建筑结构荷载规范》（GB50009-2012）中关于三面广告牌面板风载体型系数的取值和计算方法,并与正三角形三面广告牌的仿真分析结果进行比较,发现在不同的风向角下《户外广告设施钢结构技术规程》（CECS148：2003）规定的风载体型系数最小,而仿真分析得到的风荷载压力系数最大。为保证结构的安全,基于仿真分析的结果,给出了三面广告牌风载体型系数建议值;同时考虑到风荷载的非平稳性和随机性,引入风荷载的偏心距系数,为落地式三面广告牌的设计提供参考。 相似文献
16.
IMSQTI标准是一个规范测评问题模型和测试数据模型的远程教育标准,目的是提高E—learning学习系统之间的互操作和可重用。基于IMSQTI远程教育技术规范的试卷和试题库的设计方法结合了IMSQTI规范和IMSCP规范,使得规范学习试题对象可以在不同学习系统中实现重用和互操作。一个支持该方法的学习测评系统初步实现了IMSQTI试卷的编辑、分发、评分等功能。 相似文献
17.
The use of formal specification in software development is becoming increasingly prevalent. The Z nota-tion is a formal method, a language, and a style for expressing formal specification of software systems. This paperpresents a part of the specification work on a hotel guestroom reservation system. 相似文献
18.
Geometrical Product Specification and verification (GPS) is an ISO standard system covering standards of size, dimension,geometrical tolerance and surface texture of geometrical product. ISO/TC213 on the GPS has been working towards coordination of the previous standards in tolerance and related metrology in order to publish the next generation of the GPS language. This paper introduces the geometrical product specification model for design, manufacturing and verification based on the improved GPS and its new concepts,I.e., surface models, geometrical features and operations. An application example for the geometrical product specification model is then given. 相似文献
19.
MIAO Huai kou Bizuneh Bekele Teklay Tesfay 《上海大学学报(英文版)》1999,3(4):287-292
１ Ｉｎｔｒｏｄｕｃｔｉｏｎ Ｓｐｅｃｉｆｉｃａｔｉｏｎｄｅｓｃｒｉｂｅｓｔｈｅｂｅｈａｖｉｏｒｏｆｔｈｅｓｙｓｔｅｍｉｎｔｅｒｍｓｏｆｒｅｓｕｌｔｓ,ｗｈｅｒｅａｓａｎｉｍｐｌｅｍｅｎｔａｔｉｏｎｄｅｆｉｎｅｓｂｅｈａｖｉｏｒｉｎｔｅｒｍｓｏｆｐｒｏｃｅｄｕｒｅ．Ｔｈｉｓｄｉｓｔｉｎｃｔｉｏｎｇｉｖｅｓｒｉｓｅｔｏｔｈｅｉｎｆｏｒｍａｌｎｏｔｉｏｎｏｆｄｅｓｃｒｉｂｉｎｇｓｐｅｃｉｆｉｃａｔｉｏｎａｓ“ｗｈａｔ”ａｓｏｐｐｏｓｅｄｔｏｄｅｓｃｒｉｂｉｎｇｉｍｐｌｅｍｅｎｔａｔｉｏｎａｓ“ｈｏ… 相似文献