CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verification Based Failure Detection for Real-Time Java and Floating-Point Computations

Gabriele Paganelli (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2013. - 82 s.

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.

Nyckelord: Testing, Coverage, Floating-Point, Certification, Real-Time Java, Satisfiability Modulo Theories, Debugging, Formal Specification, Formal Methods

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-10-25. Senast ändrad 2015-01-12.
CPL Pubid: 185650


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)


Informations- och kommunikationsteknik

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:

Real-time java API specifications for high coverage test generation


Datum: 2013-11-21
Tid: 10:00
Lokal: room VK, Väg- och vattenbyggnad building, Sven Hultins Gata 6, Chalmers University of Technology
Opponent: Dilian Gurov, Associate Professor at the School of Science and Communications of the Royal Institute of Technology, Stockholm, Sweden.

Ingår i serie

Technical report L - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University 105