Security and Defense Contractor QinetiQ Selects AdaCore’s Mentorship Service to Upgrade to the Latest Version of the SPARK Technology
AdaCore’s Mentorship Service and SPARK Pro Selected for Modernization of QinetiQ’s Trials Control System (TCS) Software
AdaCore announced that QinetiQ has selected the AdaCore Mentorship Service to leverage its 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.
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.”