Security and Defense Contractor QinetiQ Selects AdaCore’s Mentorship Service to Upgrade to the Latest Version of the SPARK Technology

By AIT News Desk On Dec 2, 2020

AdaCore’s Mentorship Service and SPARK Pro Selected for Modernization of QinetiQ’s Trials Control System (TCS) Software

AdaCore, a trusted provider of software development and verification tools, 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.

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.

From Innovation to Infiltration: The New Cyber Threat Landscape

Nov 22, 2024

Lightning AI Raises $50Million to Simplify and Scale AI Development For Enterprises and Developers

Nov 22, 2024

Teach Mode Is Here: rabbit Gives Consumers Power to Create Custom AI Agents

Nov 22, 2024

Prev Next 1 of 40,574

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 d***** 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.”