共查询到20条相似文献,搜索用时 21 毫秒
1.
多媒体节目时序描述的组合技术 总被引:2,自引:0,他引:2
组合性是形式描述研究的基本问题,便于大型程序的设计、分析、测试和复用.为了方便用户编制大型多媒体系统的时序描述,组合模型是必须的.目前,这样的模型有基于语言的、基于图形的、基于时间区间的和面向对象的等等.但是,这些模型描述层次过低,很难支持两个多媒体节目之间的时序描述.通过引入单位流的概念和扩展两种时序关系,研究一种多媒体节目时序描述的结构化技术,使复杂的多媒体节目易于理解,以方便用户运用组合方法把一些可以复用于不同多媒体节目的节目模块进行组合设计. 相似文献
2.
3.
SPVT:一个有效的安全协议验证工具 总被引:12,自引:0,他引:12
描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性. 相似文献
4.
The process of showing that a program satisfies some particular properties with respect to its specification is called program verification. Axiomatic semantics is a verification method that makes assertions describing properties about the states of a program. There exists a transformation from the assertions of a program's verification proof to executable assertions. The latter may be embedded in the program to make it fault tolerant. An axiomatic proof system for concurrent programs is applied to generate executable assertions in a real time distributed environment. A train set example is used as modelproblem. 相似文献
5.
6.
Wai Wong 《Formal Methods in System Design》1999,14(2):193-212
Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps. 相似文献
7.
8.
Logical Specification of Reactive and Real-time Systems 总被引:1,自引:0,他引:1
9.
10.
Bernd Finkbeiner Sriram Sankaranarayanan Henny B. Sipma 《Formal Methods in System Design》2005,27(3):253-274
We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of
statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as “what
is the average number of packet transmissions' in a communication protocol, or “how often does a particular process enter
the critical section while another process remains waiting' in a mutual exclusion algorithm. To decouple the evaluation strategy
of the queries from the definition of the temporal operators, we introduce algebraic alternating automata as an automata-based
intermediate representation. Algebraic alternating automata are an extension of alternating automata that produce a value
instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic
alternating automata, we obtain a simple and efficient query evaluation algorithm. The approach is illustrated with examples
and experimental results. 相似文献
11.
12.
William R. Bevier Warren A. Hunt Jr J Strother Moore William D. Young 《Journal of Automated Reasoning》1989,5(4):411-428
The term systems verification refers to the specification and verification of the components of a computing system, including compilers, assemblers, operating systems and hardware. We outline our approach to systems verification, and summarize the application of this approach to several systems components. These components consist of a code generator for a simple high-level language, an assembler and linking loader, a simple operating system kernel, and a microprocessor design. 相似文献
13.
14.
硬件设计的形式化验证技术开辟了对复杂的超大规模集成电路设计进行验证的新途径。高阶逻辑和时态逻辑在形式化验证技术中均得到成功的应用。本文介绍用高阶逻辑表达线性时态逻辑和区间时态逻辑的方法,并以几个简单实例说明它在硬件设计验证中的应用。这种方法的优点是既利用高阶逻辑系统HOL的机械化定理证明手段,又发挥了时态逻辑的表达硬件的动态性质的能力。 相似文献
15.
An embedded system is a system that computer is used as a component in a larger device.In this paper,we study hybridity in embedded systems and present an interval based temporal logic to express and reason about hybrid properties of such kind of systems. 相似文献
16.
程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机,在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位操作指令的程序,特别是系统级代码的Hoare逻辑风格推理.本文中,二进制整数及其上的算术逻辑运算使用Coq的归纳结构演算来形式化,并且一些常见的重要性质也都使用Coq证明助理进行了严格的形式化证明. 相似文献
17.
TheSpecial Issue on Applications of Temporal Models raises many issues of time: What are the important properties of time? How can time be best represented? How can one reason about time-dependent properties? What are the important directions of temporal research? This introductory piece very briefly surveys the current wide variety of temporal models, temporal reasoning methods, and applications to time-varying phenomena. Promising areas of investigation such as the verification of concurrent systems, knowledge-base representation methods, and dealing with theFrame Problem pass in fleeting review. Brief introductions to each of the works in the volume close the section. 相似文献
18.
一种基于定理证明的Web服务合成方法研究 总被引:1,自引:0,他引:1
随着Internet中Web服务的不断增长,如何通过对现存的服务进行合成,以满足用户的个性化需求,成为目前的研究热点。通过引入线性逻辑工具,提出了一种新的Web服务合成解决方案,通过定理证明形成对应的自动服务合成流程。示例证明了该方法的有效性。 相似文献
19.
20.
实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。 相似文献