AdaCore, a trusted provider of software development and verification tools, today announced that QinetiQ has selected the AdaCore Mentorship Service to leverage their existing critical software platform investment, and address software tool obsolescence by modernizing the development environment for its Trials Control System (TCS). TCS is a command and control system designed specifically for the training, test and evaluation of military equipment.
This press release features multimedia. View the full release here: https://www.businesswire.com/news/home/20201202005035/en/
(Photo: Business Wire)
The upgrade from legacy SPARK to the latest version of the technology, SPARK 2014, was central to sustaining the safety-critical software development capability required by TCS. SPARK is a language and toolset that brings mathematics-based confidence to software verification. The latest version of SPARK provides QinetiQ with the foundation for a sound formal verification framework and static analysis toolset. One of the key features of the SPARK technology is the ability to be able to express contracts; i.e., behavioral properties that must be implemented correctly by the developer and can be checked by the verification toolset.
The Mentorship Service provides QinetiQ with hands-on guidance from AdaCore’s formal software verification experts through customized on-site training, virtual project meetings and extensive follow-up support.
Following a successful engagement, QinetiQ extended their use of the Mentorship Service. QinetiQ has also selected a multi-year subscription contract for AdaCore’s software development tools, including GNAT Pro and SPARK Pro.
“As the Lead Engineer of the QinetiQ TCS product, I can thoroughly recommend AdaCore’s Mentorship Service. Faced with the complexities of upgrading a code-base dating from 2004 and comprising several hundred thousand lines of code, I was keen to engage early on with AdaCore,” said Michael Smith, Technical Lead of Software Engineering at QinetiQ. “The Mentorship Service has proved extremely beneficial and excellent value for money. More importantly, the flexibility offered, enthusiasm and considerable expertise provided by Yannick Moy and his team have ensured that this complex upgrade remains on track and has greatly reduced the technical risks.”
“As the mentor on this project, I provided my expertise in program proof to help QinetiQ’s engineers speed up the migration process,” said Yannick Moy, SPARK Product Manager and Lead of Static Analysis at AdaCore. “As users of legacy SPARK, QinetiQ will reap even more value from migrating to the newest SPARK technology, thanks to the strong program proof guarantees that this latest version provides. The mentorship also helped the team to prove more subtle properties of code manipulating floating-point values, which are typically a challenge.”
About AdaCore Mentorship Services
Adopting any new technology requires an investment in time and energy. AdaCore’s Mentorship Services program is specifically designed to reduce these start-up costs. An AdaCore expert is assigned as a mentor who will customize the program based on need. Services can include virtual and/or on-site training sessions, project meetings to monitor project progress and discuss outstanding issues, access to tool evaluations to explore benefit to your project, direct code assistance on the customer application (if access is granted), and follow-up support. Mentorship can be purchased for a period ranging from 1 to 12 months. For more information, please visit https://www.adacore.com/mentorship.
About QinetiQ
QinetiQ is a global integrated defence and security company focused on mission-led innovation for defense, security and civil customers around the world.
We are 6,000 people creating new ways of protecting what matters most; testing technologies, systems, and processes to make sure they work as expected; and enabling customers to deploy new and enhanced-existing capabilities with the assurance they will deliver the outcomes required.
About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings:
● The GNAT Pro development environment, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability. GNAT Pro is available for Ada and also for C and C++.
● The CWE-Compatible CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software. CodePeer can detect a number of the “Top 25 Most Dangerous Software Errors” in the MITRE Corporation’s Common Weakness Enumeration (CWE).
● The SPARK Pro verification environment, a toolset providing full formal verification oriented toward high-assurance systems with stringent security requirements.
● The QGen model-based development tool suite for safety-critical control systems, providing a qualifiable and customizable code generator and static verifier for a safe subset of Simulink® and Stateflow® models, and a model-level debugger.
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial and military avionics, automotive, railway, space, defence systems, air traffic management/control, medical devices, and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/industries for further information.
AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com.
http://www.adacore.com
http://twitter.com/AdaCoreCompany
View source version on businesswire.com: https://www.businesswire.com/news/home/20201202005035/en/