首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到20条相似文献,搜索用时 234 毫秒
1.
程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。  相似文献   

2.
王海洋  段振华  田聪 《软件学报》2019,30(2):231-243
由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可用于多智能体系统(multi-agent system,简称MAS)的性质验证.MCMAS_APTL检查MAS是否满足具体性质的过程如下:首先,用解释系统编程语言(interpreted system programming language,简称ISPL)描述要验证的系统IS,用APTL公式P描述要验证的性质;然后,符号化表示系统IS,并将非P转化为范式;最后,计算所有满足非P的路径的起始状态集合.如果得到的状态集合中包含系统的初始状态,则说明系统不满足公式P;反之,则说明系统满足公式P.详细阐述了实现MCMAS_APTL的过程,并且通过验证机器人足球赛的例子展示了MCMAS_APTL的性能.  相似文献   

3.
刘椿年 《软件学报》1994,5(11):31-37
本文提出一种新的基于抽象解释的逻辑程序部分演绎方法.在一遍预处理里,针对给定的程序和目标,同时进行∪{}的部分演绎和抽象解释,以抽象解释控制部分演绎的展开过程.只要抽象论域是有穷的,部分演绎必定终止,而且'带有抽象解释估算出的关于其运行性质的信息,便于对作进一步优化.  相似文献   

4.
根据权威统计数据,软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此,应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证,需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证,提出了一种高阶类型化软件体系结构建模和验证语言(SAML)与软件体系结构建模和验证方法(SAMM).SAML语言通过定义类型和项的语法及语义,描述软件体系结构中类型和对象的构造,通过定义类型规则及其类型检查算法来判定Γ|-t:T和Γ|-RT1T2)是否成立.SAMM给出了软件体系结构建模范式,包括构建接口类型Mcls(type interface)、组件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)这5层建模过程,以及生成层内与层间类型之间关系对应的类型规则,同时定义了接口类型方法调用图(GSA)用以刻画软件体系结构设计要求,定义了类型序列及其正确性用以刻画需求期望的性质,并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS,其中,模型编辑环境支持应用软件的设计过程,验证环境支持设计满足需求的自动化验证.通过一个实际案例,完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.  相似文献   

5.
李云清 《计算机工程与应用》2001,37(23):136-138,156
对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。  相似文献   

6.
随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言(VASAML)与可验证应用系统体系结构建模方法(VASAMM).VASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t:T和Γ⊦RT1,T2)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程,包括构建Mbd(基本数据类型)、Mbti(基本接口类型)、Mdev(设备类型)和Mfrwk(应用系统框架)等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图(GDSI)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.  相似文献   

7.
本文介绍了如何通过Borland C++开发WINDOWS 3.0的应用程序,同时说明了新一代面向对象的程序设计方法OOPObject-Oriented Programming)的基本特性和实现方法。  相似文献   

8.
生物多样性保护的地理信息系统的设计   总被引:1,自引:0,他引:1  
本文介绍了关于生物多样性保护的地理信息系统的设计目标、系统构成及设计特点。该系统包括地理数据库(GBD)、制图显示系统(CDS)、数据采集系统(DCS)、数据库管理系统(DBMS)和地理分析系统(GAS)。  相似文献   

9.
基于XYZ/E描述和验证容错系统   总被引:2,自引:0,他引:2  
郭亮  唐稚松 《软件学报》2002,13(5):913-920
研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序PF;基于P,F和恢复算法R,通过容错转换给出容错程序PF-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.  相似文献   

10.
郭亮  唐稚松 《软件学报》2003,14(1):54-61
使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.  相似文献   

11.
12.
Predicate abstraction refinement is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. Thus Boolean programs are commonly employed as a simple, yet useful abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. We present a novel counterexample guided abstraction refinement procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In our procedure the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the approaches based on predicate abstraction, our approach treats arrays precisely. This is an important feature as arrays are ubiquitous in programming. We provide a precise account of the abstraction, Model Checking, and refinement processes, discuss their implementation in the EUREKA tool, and present a detailed analysis of the experimental results confirming the effectiveness of our approach on a number of programs of interest.  相似文献   

13.
李仁见  刘万伟  陈立前  王戟 《软件学报》2012,23(8):1935-1949
提出了一种链表抽象表示方法.该方法隐式存储链表结点之间的边信息,并采用了一种紧致的链表状态表示,存储开销较低,且维护了链表长度信息,精确度较高.具体而言,根据变量对链表结点的可达性质定义了变量可达向量,采用带计数的变量可达向量集描述链表的形态及数量性质,并定义了基本链表操作的抽象语义.通过简单扩展,该方法可以建模包括环形链表在内的所有单向链表.最后,为了验证该链表抽象方法的正确性,在符号执行框架中进行实验,并对常见链表操作程序的运行时错误、长度相关性质等关键性质进行了分析与验证.  相似文献   

14.
In this paper, aspects of creation of the visual programming system VIM based on filmification of application algorithms and methods are considered. Abstract self-explanatory films, which are series of frames/pictures with video, animation, audio, and other multimedia effects, are used for presentation of the method. Each frame of such a film corresponds to a certain stage, called computational step, of problem solution. A hierarchical organization of objects of such a system is suggested. The objects include both multimedia components, which demonstrate properties or an idea of the algorithm, and corresponding template programs serving for automated generation of the program created on the basis of the film specification and formulas defined by the user during the input dialog.  相似文献   

15.
In this paper,we focus on the compiling implementation of parlalel logic language PARLOG and functional language ML on distributed memory multiprocessors.Under the graph rewriting framework, a Heterogeneous Parallel Graph Rewriting Execution Model(HPGREM)is presented firstly.Then based on HPGREM,a parallel abstact machine PAM/TGR is described.Furthermore,several optimizing compilation schemes for executing declarative programs on transputer array are proposed.The performance statistics on transputer array demonstrate the effectiveness of our model,parallel abstract machine,optimizing compilation strategies and compiler.  相似文献   

16.
曹璟  徐宝文 《计算机科学》2009,36(1):256-262
类型分析是面向对象程序分析中的重要环节,精确的类型分析能够提高其它程序分析的精度.由于传统精确分析方法固有的高复杂性,现有的类型分析大都使用粗糙的分析方法.提出了一种基于SAT求解的面向对象程序类型分析方法.该方法用命题逻辑表示类型在变量间的传递关系,将程序抽象成命题公式,并使用高效的SAT求解器求解,从而获得变量运行时的类型集合.该方法是流敏感的,并且具有良好的伸缩性,既可以进行快速但精度低的上下文不敏感分析,也可以进行较慢但精度高的上下文敏感分析.  相似文献   

17.
The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can still be generated, which may prevent model-checking tools from verifying tccp programs completely. Model checking tccp programs is a difficult task due to the subtleties of the underlying operational semantics, which combines constraints, concurrency, non-determinism and time. Currently, there is no practical model-checking tool that is applicable to tccp. In this work, we introduce an abstract methodology which is based on over- and under-approximating tccp models and which mitigates the state explosion problem that is common to traditional model-checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that this preliminary abstract semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension. Finally, we complete our methodology by approximating the temporal properties that must be verified.  相似文献   

18.
We present a method for analyzing assembly programs obtained by compilation and checking safety properties on compiled programs. It proceeds by analyzing the source program, translating the invariant obtained at the source level, and then checking the soundness of the translated invariant with respect to the assembly program. This process is especially adapted to the certification of assembly or other machine-level kinds of programs. Furthermore, the success of invariant checking enhances the level of confidence in the results of both the compilation and the static analysis. From a practical point of view, our method is generic in the choice of an abstract domain for representing sets of stores, and the process does not interact with the compilation itself. Hence a certification tool can be interfaced with an existing analyzer and designed so as to work with a class of compilers that do not need to be modified. Finally, a prototype was implemented to validate the approach.  相似文献   

19.
This paper reports on an exemplary study of the performance of commercial computational fluid dynamic (CFD) software programs when applied as engineering tool for microfluidic applications. Four commercial finite volume codes (CFD-ACE+, CFX, Flow-3D and Fluent) have been evaluated by performing CFD-simulations of typical microfluidic engineering problems being relevant for a large variety of lab-on-a-chip (LOAC) applications. Following problems are considered as examples: multi lamination by a split and recombine mixer, flow patterning on a rotating platform (sometimes termed “lab-on-a-disk”), bubble dynamics in micro channels and the so called TopSpot® droplet generator for micro array printing. Hereby mainly the capability of the software programs to deal with free surface flows including surface tension and flow patterning of two fluids has been studied. In all investigated programs the free surfaces are treated by the volume-of-fluid (VOF) method and flow patterning is visualised with a scalar marker method. The study assesses the simulation results obtained by the different programs for the mentioned application cases in terms of consistency of results, computational speed and comparison with experimental data if available.  相似文献   

20.
Model Checking Dynamic Memory Allocation in Operating Systems   总被引:1,自引:0,他引:1  
Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.  相似文献   

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

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