- AdaCore - YouTube
- Refactoring with confidence: A pattern-based approach built on top of LibAdaLang to save money
A challenge that every code base will phase over time are code smells. AdaCore provides tooling to find smells in code, like GNATcheck and CodePeer. Newly applied to a code base the number of findings of this tools can be big. Bigger than one can solve with limited resources. We will present an approach based on LibAdaLang to fix code smells automatically saving you many hours of rewriting code manually. This approach is pattern based and can thus be applied to generic transformations of a code base.
As the regulatory framework in the United States and Europe evolves to address increasingly growing cybersecurity threats, AdaCore is enlarging the scope of its offering to help you meet these challenges. In addition to its longstanding commitment to formal proof and static analysis, AdaCore is now upgrading its product security procedures and preparing a dynamic analysis solution. This presentation will give an insight into our roadmap in both areas, and showcase the upcoming fuzzing technology.
- AdaCore - YouTube
- Streamline Certification using QGen TQL-1 Qualifiable Auto Code Generator for Simulink®/Stateflow®
Presented by S. Tucker Taft - AdaCore
This session will introduce the QGen Auto Code Generator for Simulink®/Stateflow® and explain the advantages provided by a TQL-1 Qualification, in terms of reduced time and effort to certify a Simulink-based application. The talk will identify the DO-178C and DO-331 objectives that are covered by the QGen code generator, meaning that your team can avoid many of the most labor-intensive steps involved in achieving certification, even at the highest level of criticality. The talk is aimed at both engineers and managers for such critical systems development activities and will cover the features of the QGen code generator, as well as other tools with which it is integrated, including a model-level debugger and testing tools for Simulink-based applications running in embedded targets.
Implementation and verification are traditionally viewed as two separate activities. Even in test-driven environments, the test platform is distinct from the implementation one. This talk will present an alternative approach where the verification and development activities are engineered together, creating effectively a “self-verified” program combining at the same place an implementation and the means to verify its correctness.
4 key takeaways
- Developing verification at the same time as the code allows for more efficient coding processes and mitigates errors at the end of the process.
- Formal proofs and testing can be combined to increase the level of safety and decrease overall development costs.
- There are alternatives to the C programming language that allows more effective verification.
- There is a way to redirect software developers energy from worrying about low-level coding errors to concentrate on more valuable aspects of software engineering.
Presented by Quentin Ochem at ScaleUp OSS.5 Europe Day.
This demo, presented by Albert Lee, shows how a FACE™ software component ("UoC", or "Unit of Conformance") written in Ada can be verified for FACE conformance, using a combination of link-time tests in the CTS (Conformance Test Suite) and source-code analysis by AdaCore's GNATcheck static analysis tool.
Modernization efforts that require consolidating multiple proven software systems onto a single intelligent edge platform are difficult. Fortunately, there are strategies that allow you to maintain your software integrity and partitioning while taking advantage of cutting edge software development technology.
In this webinar, subject matter experts from Wind River and AdaCore will demonstrate how you can map your existing architecture to guest operating systems on hypervisors, by using Wind River’s Helix Virtualization Platforms and software development tools from the compiler experts at AdaCore.
- AdaCore - YouTube
- NVIDIA — Securing the Future of Safety and Security of Embedded Software (Captioned)
SPARK / Ada Journey to Adoption
As software becomes more complex, the chances of human error greatly increase, opening up potential for security and safety risks. NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.
0:00 - Intro by Patrick Mannion
2:10 - Business context for Ada and SPARK at NVIDIA by Daniel Rohrer
18:41 - Technical aspects of NVIDIA's adoption of SPARK by Dhawal Kumar
19:33 - Firmwares and their environment
21:01 - What is this SPARK that we've all been raving about?
29:35 - SPARK alternatives considered (and dismissed)
36:35 - Proof of Concept — It's conclusions and concerns
45:38 - Benefits and Summary
48:37 - Q and A
GNAT Studio is a powerful and intuitive IDE that supports the full development workflow, from coding to system integration, testing, debugging, and code analysis. It is particularly well-suited for programmers using Ada, SPARK, C and C++.
This year the interface remains the same on the outside, but we have a new engine behind GNAT Studio: the Ada Language Server (ALS). This new engine is based on Libadalang and isn't compiler-dependent, compared to our previous technology that depended on ALI files generated from a compilation. ALS uses the Microsoft Language Server Protocol (LSP), that defines a standard communication method to connect development tools with local language servers. This common framework makes it easy for IDEs to support more languages, and it makes it possible for language-specific code to be reused. It also gives the possibility to not use GNAT Studio at all and enjoy Ada functionality in a number of other IDEs.
Check out this video to see how these new changes make GNAT Studio more efficient, more reliable, and more maintainable.
The CodePeer Tool Suite is a set of static analysis tools for the Ada programming language designed to help developers, reviewers, and testers detect bugs and vulnerabilities in Ada code. The tool suite includes the CodePeer advanced static analysis tool, the GNATcheck coding standard checking tool, the GNATmetric statistical analysis tool, and the GNAT Studio IDE which give developers a comprehensive view of the health and quality of their source code from an integrated and modern development environment.
AdaCore's release of version 21.0 of the CodePeer Advanced Static Analysis Tool Suite is here! The release includes a multitude of new features, in addition to bug fixes and stability enhancements to improve the tools' user experience.
Check out this video to get a quick overview of the tool suite, see the new features integrated into the new release of the technology, and get an understanding of how the CodePeer Advanced Static Analysis Tool Suite can improve your software development life cycle.
SPARK Pro is a language and toolset that allows developers to formally define and automatically verify software requirements to guarantee that a program behaves as intended. You can adopt SPARK either at the beginning of a project, or by progressively integrating it in an existing codebase developed, for example, in Ada, C or C++.
AdaCore’s release of SPARK Pro 21.0 expands its support of Ada language constructs, allowing more programs to be effectively specified and verified, and provides better tool interactions with improved tool messages and guidance.
Check out this video to discover how the latest capabilities in SPARK 21.0 can help you save time and effort while reaping the full benefits of formal program verification.
GNATcoverage is an all-in-one code coverage analysis tool. It thoroughly tracks the execution of your program and records this information in a trace file.
This year, GNATcoverage offers source code instrumentation capabilities that make code analysis more accessible, more versatile, and much, much faster on native platforms. It also allows the technology to be used across the board, alongside on all targets and all versions of the GNAT Pro technology.
We’re excited to show you what GNATcoverage can do. Check out this video to learn just how easy GNATcoverage is to use, and how the new capabilities can help you meet the highest software quality standards.
GNAT Pro is a robust and flexible Ada, C and C++ development environment. It comprises a toolchain based on the GNU GCC technology; an Integrated Development Environment (GNAT Studio); a comprehensive toolsuite, including a visual debugger; and a set of libraries, bindings and tools.
GNAT Pro is upgraded annually, and Version 21.0, released earlier this month, adds support for a number of new platforms, including VxWorks 600+ on x86 / ARM / PowerPC; C++ availability on all VxWorks 7 ports; Windows-hosted Linux cross for ARM (PowerPC is also available); and RISC-V 32 on bare metal. Version 21.0 also adds a number of key features, including a more powerful CCG (Common Code Generator), new Libadalang capabilities for Ada code analysis, and support for key features of the Ada 202X standard. All of these upgrades are designed to better support multi-language and safety-critical development as well as security vulnerability resilience.
Check out this video to learn how GNAT Pro’s new platforms, tools and libraries can help kick your workflow up to the next level.
Sensor fusion software is unique with its combination of firmware-like layers, responsible for reading and validating sensor data, and higher-level algorithmic software, responsible for producing synthesized, actionable data. Because of the criticality of these systems, they require extensive testing and verification to increase confidence that the computed data can be trusted. From a software development point of view, the traditional approach is to rely on the C or C++ programming language, and to offset its inherent safety vulnerabilities by using expensive tooling and human-based processes. In this presentation we will present an alternative approach, through the usage of a different programming language which was designed for safety critical systems and gives developers tools to write safe and secure firmware, as-well-as, robust high-level algorithmic code with the same ecosystem of language and tooling. Topics covered:
- Overview of Ada and SPARK language features for firmware development
- Overview of Ada and SPARK language features for algorithm and high-level software development
- Overview of formal proof and how it differs from traditional static analysis techniques
- Integration with existing C code bases
- Performances considerations
- ISO 26262 considerations and benefits
- Resources for Ada and SPARK in the software community
GNATtest helps automate the essential, but tedious and error-prone, processes for developing and managing the large number of test cases needed for verifying large software systems.
Learn more at https://www.adacore.com/gnatpro/toolsuite/gnattest