共查询到20条相似文献,搜索用时 93 毫秒
1.
基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Java,并且全面支持动态和静态的契约检查.首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例. 相似文献
2.
针对Java实时规范中的非堆内存抽象,讨论实现中的不确定因素以及运行时不可预测的时间特性,提出并实现了一种用于硬Java实时平台的非堆内存模型.模型基于硬Java实时平台预处理机制的支持,采用一种基于静态约束的安全访问检查算法,将运行时单亲规则及赋值规则检查等影响系统实时性的操作在运行前完成,保证了运行时的可预测.同时,针对当前关于静态分析方法研究中多不支持作用域多线程共享的现状,模型在不改变实时Java句法及编程模式的前提下,保留了对作用域多线程共享的支持. 相似文献
3.
刘烨 《计算机光盘软件与应用》2013,(6):231-232
本文通过参数化扩展上下文无关文法作为其安全相关行为模型的抽象表示,针对Java多线程序研究,总结出了从多线程Java程序自动生成安全相关行为模型的方法,该方法应用到携带模型代码方法的实现框架中,形象的描述了静态检查该模型是否满足安全策略的实现,同时为安全执行非信任多线程Java移动代码提供了有效支持。本文合理的使用静态分析多线程Java程序的措施,来进行相关安全性的检查,从中来考察出多线程Java程序的相关安全行为。 相似文献
4.
5.
姚铮 《计算机光盘软件与应用》2014,(10):146-146
在当前静态分析技术对于分析算法有着重要的影响,由于其方法比较复杂这就出现了精度不高,因此本文针对在静态分析中存在的实际问题进行具体的研究,能够从其问题中提出改进的方案,并且采用动态分析技术构造Java程序的动态调用图,文章中采用k-类方法后向切片计算修改影响的集合,之进行具体的试验,提高了精度,该技术的革新便于在大型Java程序中进行应用,改善了测试效果。 相似文献
6.
7.
高德龙 《数字社区&智能家居》2009,(11)
对Java程序设计中出现的异常处理技术进行了研究,对Java异常处理知识进行了必要的介绍和简单的分析,并总结了几种在Java程序设计中如何定义和使用异常类。 相似文献
8.
9.
10.
11.
Context: Static analysis of source code is a scalable method for discovery of software faults and security vulnerabilities. Techniques for static code analysis have matured in the last decade and many tools have been developed to support automatic detection.Objective: This research work is focused on empirical evaluation of the ability of static code analysis tools to detect security vulnerabilities with an objective to better understand their strengths and shortcomings.Method: We conducted an experiment which consisted of using the benchmarking test suite Juliet to evaluate three widely used commercial tools for static code analysis. Using design of experiments approach to conduct the analysis and evaluation and including statistical testing of the results are unique characteristics of this work. In addition to the controlled experiment, the empirical evaluation included case studies based on three open source programs.Results: Our experiment showed that 27% of C/C++ vulnerabilities and 11% of Java vulnerabilities were missed by all three tools. Some vulnerabilities were detected by only one or combination of two tools; 41% of C/C++ and 21% of Java vulnerabilities were detected by all three tools. More importantly, static code analysis tools did not show statistically significant difference in their ability to detect security vulnerabilities for both C/C++ and Java. Interestingly, all tools had median and mean of the per CWE recall values and overall recall across all CWEs close to or below 50%, which indicates comparable or worse performance than random guessing. While for C/C++ vulnerabilities one of the tools had better performance in terms of probability of false alarm than the other two tools, there was no statistically significant difference among tools’ probability of false alarm for Java test cases.Conclusions: Despite recent advances in methods for static code analysis, the state-of-the-art tools are not very effective in detecting security vulnerabilities. 相似文献
12.
An overview of JML tools and applications 总被引:3,自引:0,他引:3
Lilian Burdy Yoonsik Cheon David R. Cok Michael D. Ernst Joseph R. Kiniry Gary T. Leavens K. Rustan M. Leino Erik Poll 《International Journal on Software Tools for Technology Transfer (STTT)》2005,7(3):212-232
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification typechecking, runtime debugging, static analysis, and verification.This paper gives an overview of the main ideas behind JML, details about JML’s wide range of tools, and a glimpse into existing applications of JML. 相似文献
13.
代码质量度量是软件质量分析的一个重要研究方向。静态分析方法因其具有成本低、容易实现而且不依赖于程序特定的运行环境的优点,在当前软件网络化、服务化的趋势下倍受关注。针对Java代码质量度量进行研究,使用Ant工具整合各种开源的静态测试工具,并制定基于静态分析的Java代码质量综合评价方案,可支持包括代码规模、规范性、可维护性、可扩展性和潜在危险等方面的综合检测,为项目的开发者、管理者和使用者提供了实用的代码质量评价方法。 相似文献
14.
Thomas Bøgholm Christian Frost René Rydhof Hansen Casper Svenning Jensen Kasper Søe Luckow Anders P. Ravn Hans Søndergaard Bent Thomsen 《Innovations in Systems and Software Engineering》2013,9(1):17-28
We present a rationale for a selection of tools that assist developers of hard real-time applications to verify that programs conform to a Java real-time profile and that platform-specific resource constraints are satisfied. These tools are specialised instances of more generic static analysis and model checking frameworks. The concepts are illustrated by two case studies, and the strengths and the limitations of the tools are discussed. 相似文献
15.
In Java software, one important flexibility mechanism is dynamic class loading. Unfortunately, the vast majority of static
analyses for Java treat dynamic class loading either unsoundly or too conservatively. We present a novel semi-static approach
for resolving dynamic class loading by combining static string analysis with dynamically gathered information about the execution
environment. The insight behind the approach is that dynamic class loading often depends on characteristics of the environment
that are encoded in various environment variables. Such variables are not static elements; however, their run-time values
typically remain the same across multiple executions of the application. Thus, the string values reported by our technique
are tailored to the current installation of the system under analysis. Additionally, we propose extensions of string analysis
to increase the number of sites that can be resolved purely statically, and to track the names of environment variables. An
experimental evaluation on the Java 1.4 standard libraries shows that a state-of-the-art purely static approach resolves only
28% of non-trivial sites, while our approach resolves 74% of such sites. We also demonstrate how the information gained from
resolved dynamic class loading can be used to determine the classes that can potentially be instantiated through the use of
reflection. Our extensions of string analysis greatly increase the number of resolvable reflective instantiation sites. This
work is a step towards making static analysis tools better equipped to handle the dynamic features of Java.
This material is based upon work supported by the National Science Foundation under CAREER grant CCF-0546040. 相似文献
16.
17.
Cesar Couto João Eduardo Montandon Christofer Silva Marco Tulio Valente 《Software Quality Journal》2013,21(2):241-257
Despite the interest and the increasing number of static analysis tools for detecting defects in software systems, there is still no consensus on the actual gains that such tools introduce in software development projects. Therefore, this article reports a study carried out to evaluate the degree of correspondence and correlation between post-release defects (i.e., field defects) and warnings issued by FindBugs, a bug finding tool widely used in Java systems. The study aimed to evaluate two types of relations: static correspondence (when warnings contribute to find the static program locations changed to remove field defects) and statistical correlation (when warnings serve as early indicators for future field defects). As a result, we have concluded that there is no static correspondence between field defects and warnings. However, statistical tests showed that there is a moderate level of correlation between warnings and such kinds of software defects. 相似文献
18.
《Science of Computer Programming》2008,70(1-3):14-26
The JastAdd system enables modular specifications of extensible compiler tools and languages. Java has been extended with the Rewritable Circular Reference Attributed Grammars formalism that supports modularization and extensibility through several synergistic mechanisms. Object-orientation and static aspect-oriented programming are combined with declarative attributes and context-dependent rewrites to allow highly modular specifications. The techniques have been verified by implementing a full Java 1.4 compiler with modular extensions for non-null types and Java 5 features. 相似文献
19.
In Java, type resolution is a function that takes a reference to a type occurring in a given context as input and returns the canonical name of that type. This information is fundamental to static analysis—a “must have” function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle. 相似文献
20.
The creation, transformation and analysis of bytecode is widespread. Nevertheless, several problems related to the reusability and comprehensibility of the results and tools exist. In particular, the results of tools for bytecode analysis are usually represented in proprietary tool dependent ways, which makes it hard to build more sophisticated analysis on top of the results generated by tools for lower-level analysis.Furthermore, intermediate results, such as e.g., the results of basic control flow and dataflow analysis, are usually not explicitly represented at all; though, required by many more sophisticated analysis. This lack of a common format, for the well structured representation of the (intermediate) results of code analysis, makes the creation of new tools or the integration of the results generated by different tools costly and ineffective.To solve the highlighted problems, we propose a higher-level XML-based representation of Java bytecode which is designed as a common platform for the creation and transformation of bytecode and explicitly enables the integration of arbitrary information generated by different tools for static code analysis. 相似文献