Verification Based Failure Detection for Real-Time Java and Floating-Point Computations
Sammanfattning: To err is human, and machines help us avoiding errors. This thesis presents two ways, based on verification technology, to prevent failures. Safety critical Real-Time Java applications usually need a certification. Tests fulfilling specific coverage criteria can be part of such certification, like in the DO-178 standard. This thesis presents the KeYTestGen tool, an automated test case generator fulfilling certification-demanded coverage criteria by construction. The work also develops a formal specification of the Real-Time Java API to direct the search for input values and generate code that checks the expectations on the tests. The KeYTestGen tool found an inconsistency between a commercial Real-Time Java implementation and its specification; and there are evidences that employing KeYTestGen can shorten the testing time up to 72% of the allocated time. Floating-point computations are spreading in safety-critical systems, but numerical computing skills are rare: hence the demand of program analysis methods for developers untrained in numerical computing. A simple way to detect problems in a floating-point computation is to run a program twice, using different floating-point precisions: a program is said unstable when the result computed with lower precision is far from the result computed with higher precision - how "far" depends on the context. The proposed analysis method detects instability of a program at compile-time for any pair of IEEE-standard-like formats. It is independent from the concrete choice of programming language or compiler. The FPhile verification system implements the method, using floating-point specific Satisfiability Modulo Theory (SMT) solvers. Experimental results found instability where random testing could not.
Denna avhandling är EVENTUELLT nedladdningsbar som PDF. Kolla denna länk för att se om den går att ladda ner.