Welcome to JORAL Technologies Safety Critical Tool Department.
This department is set up to support Software Engineers dealing with Safety Critical Applications. We offer free product demonstrations for all products.
General Jenkins Continuous Integration plugin now available for a³ and Astrée. The safety manual now also covers regulations for medical devices, in particular the FDA Principles of Software Validation. The safety manual now describes qualified tool workflows for a³ and Astrée.
Astrée: Astrée now also reports all potential deadlocks. New domain for precise handling of process priorities including dynamic priorities, e.g., according to the Priority Ceiling Protocol. A new data flow view enables users to efficiently explore data races. The analyzer now supports pointers of different sizes, e.g., near/far/huge pointers. Most semantic MISRA rules now can be checked without running the sound run-time error analysis. New customizable HTML reports available.
aiT, TimingProfiler, StackAnalyzer, ValueAnalyzer
New targets: StackAnalyzer/ValueAnalyzer now available for TI MSP430(X). aiT for ARM supports Infineon XMC4500 (Cortex-M4F). aiT for C28x supports additional cores: TMS320F28035, TMS320F28335 and TMS320F28069. a³ now saves the current analysis state inside a workspace. All graphs, statistics and other outputs can be reviewed in the GUI without running the analysis again. The analyses provide AIS2 "annotation hints" for common analysis problems in the reporting and in the GUI (message view and graph). The GUI allows to interactively add per mouse-click the provided annotation hints to the project. Further AIS2-annotations can now be automatically added to the project from the graphs, statistics views and the AIS editors via the context menu. - A new statistics view shows minimum and maximum loop bounds for all loops.
CompCert The CompCert installer now offers a GUI to compile the runtime libraries for the provided target configurations. New command line options for more control of diagnostic output of CompCert.
Two new plugins for a³ and Astrée enable automatic integration of aiT, StackAnalyzer, TimingProfiler, and Astrée in Jenkins, the leading open-source continuous-integration framework. After a one-click installation, you can - configure an analysis run as a Jenkins build step - automatically mark build steps depending on the analysis results - generate analysis reports directly in the Jenkins workspace - access analysis results via the Jenkins web interface.
For more information and download links, see: http://www.absint.com/astree/jenkins.htm http://www.absint.com/a3/jenkins.htm
2.) Integration of the Astrée Rule Checker into Eclipse
Our partner Konzept-IS provides a plugin that allows you to run Astrée’s coding-rule checker directly from within the Eclipse IDE.
For more information, see: https://www.absint.com/astree/kerci.htm
AbsInt provides unique tools and services for the development, analysis, and certification of safety-critical software.
*Astrée* for proving the absence of runtime errors and data races in C and for checking compliance with MISRA, CWE, CERT, and ISO coding rules. https://www.absint.com/astree *CompCert*, the only formally verified optimizing C compiler, for meeting the highest standards of software assurance. https://www.absint.com/compcert *aiT Worst-Case Execution Time Analyzer* for obtaining timing guarantees, precisely taking the processor architecture into account. https://www.absint.com/ait *TimingProfiler* for obtaining execution-time estimates of programs without the need to repeatedly provide test inputs, execute, and measure. https://www.absint.com/timingprofiler *StackAnalyzer* for proving the absence of stack overflows by computing the worst-case maximum stack usage of tasks. https://www.absint.com/stackanalyzer
All our verification tools can be qualified according to contemporary safety standards.