Joral Technologies Inc.

Here is an Online video demonstrating the new KEIL DS-MDK Development tools working with the

NXP ARM® Cortex®-A7 Core, ARM Cortex-M4 Core.

1.) Jenkins Plugin for a³ and Astrée

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

3.) Upcoming Events

dSPACE Technology Conference 2016, 13–14 September, Naperville, Illinois, USA Automotive Software Congress, 21–22 September,

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.

NXP i.MX 6SoloX SABRE Reference

Learning Platform

This page contains information and links that help you to create
your own Linux image on the i.MX 6SoloX SABRE board in order to
be able to debug your system with DS-MDK and ULINKpro.
The following buttons let you download a pre-configured Linux
image for use with DS-MDK, as well as the debug symbols and the
kernel sources for Linux kernel debugging.
LINKS

NXP i.MX 7 Reference
Learning Platform
This page contains information and links that help you to create
your own Linux image on the i.MX 7 SABRE board in order to be able
to debug your system with DS-MDK and ULINKpro.
The following buttons let you download a pre-configured Linux
image for use with DS-MDK, as well as the debug symbols and the
kernel sources for Linux kernel debugging. All are based on the
Freescale Community BSP
LINKS

Using ST-Link/V2 and MDK 5 with Discovery/Nucleo Boards

This hands-on lab demonstrates the use of the STMicroelectronics ST-Link/V2
debug adapter and Keil uVision. The lab uses the STM32F401C Discovery Kit
but it can be adapted to use other STMicroelectronics processors that work
with the ST-Link/V2 adapter. The program examples provided in the
Keil.STM32F4xx_DFP device family software pack may be downloaded from the
Keil MDK5 Software Packs website. All examples are compliant to Cortex
Microcontroller Software Interface Standard (CMSIS v4.5). These examples
demonstrate the use of Serial Wire Viewer (SWV) and Debug Access Port (DAP)
debug technology, memory reads and writes, Instrumentaiton Trace Macrocell
(ITM) and the RTX Kernel Awareness Viewer.

CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical
and mission-critical software written in C and meeting high levels of assurance. It ac­cepts most of
the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM,
PowerPC, and x86 architectures.