(转)安全Java标准草案静态属性分析

bilbo0214

Analysis of Static Properties in a Draft Standard for Safety-Critical Java
file:///C|/Working/www.rtcgroup.com/cotsjournal/images/v2/spacer.gif
Many of the strengths that have contributed to Java’s success also benefit static hard real-time and safety-critical systems. By restricting the use of Java language features and libraries, and establishing conventions to standardize the static property annotations of Java programs to enforce consistency, many of Java’s benefits can be applied to safety-critical development.
file:///C|/Working/www.rtcgroup.com/cotsjournal/images/v2/spacer.gif
By Kelvin Nilsen, CTO,Aonix
file:///C|/Working/www.rtcgroup.com/cotsjournal/images/v2/spacer.gif
The Java language has been widely heralded for its programmer productivity gains in enterprise and desktop applications. Productivity gains stem largely from Java’s dynamic programming capabilities that enable developers to include features such as dynamic class loading and JIT compilation. which accelerate the develop-test-debug cycle. In addition, automatic garbage collection simplifies the task of managing dynamic memory allocation. These dynamic features often stand out in developers’ minds as the key reasons why the Java language allows them to be approximately twice as productive as C++ developers.
It turns out, however, that Java’s dynamic features represent only part of the reason why Java developers are more productive than C++ developers. In comparison with C++, the Java compilers and linkers also perform more static property analysis, which enforces stronger consistency checking within software systems. This stronger consistency checking further improves developer productivity by reducing programming errors. It is also especially helpful when large software systems are assembled from components independently produced by different teams of developers. Examples of Java’s built-in static property enforcement include:
• Strong type checking prohibits incompatible type coercion between, for example, an integer and a reference type, or between two incompatible reference types.
• Programmers are prohibited from adding integer values to reference values to create references to new objects.
• Byte code verification that ensures the types of actual parameters passed to a method invocation exactly match the types of the formal parameters declared for the invoked method.
• Compilers and byte code verifiers explicitly require contexts that invoke methods that might throw “checked exceptions” to deal explicitly with that possibility.
Because of the strong static property checking already enforced by the programming environment, Java has attracted the attention of safety-critical developers as a possible language of choice. Safety-critical software includes applications such as anti-lock braking systems in consumer vehicles, fly-by-wire control of flight surfaces in commercial aircraft, automatic shutdown of nuclear power plants and computer-controlled switching systems in passenger railroad stations. Such applications are certified as reliable and correct according to various protocols, depending on the regulating government agency responsible for the particular industry. All of the certification techniques share a common goal: to prove through analysis of the static properties of the software that it will always run correctly.
A draft specification for safety-critical Java is being developed by the Embedded and Real-Time Systems Forum of the Open Group in an effort to create a standard that is endorsed both by the Java Community Process and by the ISO. This standard is based on the traditional Java platform as extended by the official Real-Time Specification for Java (RTSJ).
However, dynamic features such as dynamic class loading, automatic garbage collection, and the RTSJ’s concept of ScopedMemory regions, have all been removed. To this stripped-down base, certain enhancements will be added to provide even more static verification than is available in traditional Java. Programmers who develop their code according to the published safety-critical guidelines can rely on assurances from the safety-critical Java compiler that:
• The maximum amount of CPU time required to execute particular methods (and all overriding methods) is bounded by a constant that can be derived as a static property of the program and knowledge of the target hardware.
• The maximum amount of stack memory required to execute particular methods (and all overriding methods) is bounded by a constant that can be derived as a static property of the program and knowledge of the target hardware.
• Execution of a particular method (or of any overriding method) will not allocate any memory in the shared immortal heap. (Since the safety-critical Java environment has no automatic garbage collector, any objects allocated in the heap are considered to be immortal, because their memory will never be reclaimed.)
• Execution of a particular method will not result in throwing of RTSJ-defined CeilingViolationException, DuplicateFilterException, IllegalAssignmentError, InaccessibleAreaException, MemoryAccessError, MemoryScopeException, MemoryTypeConflictException, OutOfMemoryError, ScopedCycleException, StackOverflowError or ThrowBoundaryError exceptions.
Since space does not permit a description of all aspects of the safety-critical Java specification, we will focus on the analysis of static properties in a sample safety-critical Java program.
Figure 1 represents source code for an analyzable bubble-sort program. In this program, Java 5.0-style meta-data annotations and assertions allow developers to specify static properties associated with their programs. The @StaticAnalyzable annotation in line 10 denotes that the worst-case execution time and the worst-case memory allocation needs for the sort() method introduced on line 11 must be analyzable as a static property of the program. Note that the @StaticAnalyzable annotation is accompanied by two attributes—enforce_analysis and modes. The modes attribute represents an enumeration class that identifies the various modes of operation for this method’s execution. Analysis of the method’s static resource requirements depends on the mode under which it is executing.

Figure 2 shows the declaration of the AnalysisModes enumeration. In this case, there are five different modes of operation. The first mode, named UNBOUNDED, represents a situation in which the size of the array passed as an argument to the sort() method is not known as a static property of the caller’s context. In this mode of operation, the resource needs cannot be analyzed, and this is represented by a false value in the first entry of the enforce_analysis array.

The other modes of operation, named SMALL, BIG, SMALL_PRESORTED and BIG_PRESORTED, represent the corresponding initialization value in the enforce_analysis array’s initializer, which evaluates to true. In the SMALL mode of operation, the array argument is assumed to have fewer than 16 elements. In the BIG mode of operation, the array argument is assumed to have fewer than 64 elements. SMALL_PRESORTED and BIG_PRESORTED correspond to similarly sized arrays in which all elements except one of the incoming array are known to be in sorted order.
In analyzing the CPU time required to complete execution of the sort() method, we expect SMALL_PRESORTED to execute in less time than BIG_PRESORTED, which will execute in less time than SMALL, which will execute in less time than the BIG mode of operation. Whenever the sort() method is called from a context that is itself analyzable, the calling context must define the mode of operation under which it expects the sort() method’s resource requirements to be analyzed. This is accomplished by preceding the invocation with an assertion that specifies the intended mode of operation for the called method, as shown in Figure 3.

In this example, the sort() method is to be analyzed according to the SMALL_PRESORTED mode of operation. Note that the initialization expression for the array (line 12) creates an array with six elements, only one of which is out of sequential order. If the assertion in line 14 of Figure 3 had been omitted, the sort() method would have been analyzed according to the rules of the first entry in the AnalysisModes enumeration. Since, in this case, the corresponding entry in the sort() method’s enforce_analysis attribute is false, the safety-critical Java compiler would reject this program as invalid because the caller’s context requires analyzability of all called methods.
The assertions provided in the body of the sort() method (Figure 1) are sufficient to limit the number of iterations consumed in each of the analysis modes except for UNBOUNDED. The assertion in line 19, for example, denotes that the innermost nested loop (the one that begins on line 16) will iterate no more than twice if this method is being executed in analysis mode SMALL_PRESORTED. The NestedIterationBound assertion in line 26 signifies that the body of code that includes this assertion will execute no more than 29 times for each entry into the outer loop at outer-nesting level one if the sort method is being analyzed according to the SMALL_PRESORTED analysis mode. Similarly, the NestedIterationBound assertion at line 29 requires that the enclosing body of the if-then statement executes no more than 15 times for each entry into the outer-nested if this method is being analyzed according to the SMALL_PRESORTED mode of execution.
Enforcement of Static Properties
A difficulty lies in the fact that it is not possible in the most general case for a compiler to enforce the validity of all programmer-supplied assertions. Programmers might, for example, claim that they are passing a small array to the sort() method, when they are really passing an array with more than 1000 elements. Or programmers might assert that a particular loop will execute no more than 100 times for a given configuration of input values, when they might have misrepresented or misunderstood the complexity of certain algorithms.
The primary objectives of the static property analysis in the draft safety-critical Java specification are to enable programmers to make very clear their intentions regarding the static properties associated with particular components. This enables the automatic enforcement of consistency between the static properties of independently created components, and eliminates much of the tedium associated with analyzing worst-case execution times, stack growth and heap memory allocation.
Enforcement of static software properties in the safety-critical Java specification takes two specific forms:
1. The compiler, byte-code verifier and linker work together to ensure that all programmer-declared assertions are internally consistent. This means that if a particular component is declared to be analyzable, any components it depends on must also be declared to be analyzable and the results of analysis must satisfy all programmer-declared requirements.
2. If the program is compiled with assertions enabled, an assertion exception will be thrown any time the program behaves in such a way as to violate any of the assertions that describe the static properties intended by the programmer.
In a safety-critical system, a separate proof mechanism is required to ensure that each component satisfies the static properties described in the programmer-supplied annotations. In particular, it must be proven that the bounds on loop iterations are valid for every possible set of input values that is consistent with each method’s available analysis modes. Further, it must be shown that every invocation of an analyzable method establishes the value of the method’s analysis mode to a constant value. That value must appropriately represent the complexity of executing the invoked method based on context-sensitive knowledge of the input values that will be passed as parameters to the method.
Such proofs are required in all safety-critical development. Some of these proofs can be automated using automatic theorem proving technologies based on, for example, JML (Java Modeling Language). In the most general cases, generating these proofs cannot be entirely automated because automatic proving of arbitrary theorems is considered “not computable.” This is why the proposed safety-critical Java language standard restricts its automatic static property analysis to the realm of static property checking and consistency enforcement that can be easily and efficiently solved by compilers and other static analysis tools.
Aonix
Malakoff Cedex.
France.
+33 (0)1 41 48 11 05.
[www.aonix.com].


本文来自ChinaUnix博客，如果查看原文请点：http://blog.chinaunix.net/u/29291/showart_365515.html