VeriFlux is a
formal methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expec ...
based static analysis tool for programs written in Java. It is optimized for use with
JamaicaVM
The JamaicaVM is a virtual machine and build environment for developing and running realtime Java programs. It includes a deterministic garbage collector and implements the RTSJ.Fridtjof Siebert, "Realtime Garbage Collection in the JamaicaVM 3.0 ...
, but can be used for any Java program. It can detect uncaught runtime exceptions, including
RTSJ
Real time Java is a catch-all term for a combination of technologies that enables programmers to write programs that meet the demands of real-time systems in the Java programming language.
Java's sophisticated memory management, native support ...
exceptions, and possible deadlocks in code using Java synchronization features. It has also been used for resource analysis.
[James J. Hunt, Isabel Tonin, Fridtjof Siebert: Using Global Data Flow Analysis on Bytecode to Aid Worst Case Execution Time Analysis for Realtime Java Programs. JTRES 2008: 97-105] It can be used for both full program analysis and partial program analysis.
See also
*
Aicas
aicas GmbH is a software corporation headquartered in Germany with subsidiaries in France and the United States.
aicas provides Java technology and analysis tools for realtime and embedded systems. Its flagship product is JamaicaVM, a Java Virtu ...
*
JamaicaVM
The JamaicaVM is a virtual machine and build environment for developing and running realtime Java programs. It includes a deterministic garbage collector and implements the RTSJ.Fridtjof Siebert, "Realtime Garbage Collection in the JamaicaVM 3.0 ...
*
Formal Methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expec ...
*
Data Flow Analysis
In the pursuit of knowledge, data (; ) is a collection of discrete values that convey information, describing quantity, quality, fact, statistics, other basic units of meaning, or simply sequences of symbols that may be further interpreted. ...
*
Real time Java
Real time Java is a catch-all term for a combination of technologies that enables programmers to write computer program, programs that meet the demands of real-time computing, real-time systems in the Java (programming language), Java programming ...
*
Embedded Java
Embedded Java refers to versions of the Java program language that are designed for embedded systems. Since 2010 embedded Java implementations have come closer to standard Java, and are now virtually identical to the Java Standard Edition. Since ...
References
External links
*{{Official website, www.aicas.com/veriflux.html
Static program analysis tools