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 modernising 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 Mentorship Service has proved extremely beneficial and excellent value for money... this complex upgrade remains on track and has greatly reduced the technical risks."
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., behavioural 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 customised 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.
About QinetiQ
QinetiQ is a global integrated defence and security company focused on mission-led innovation for defence, security and civil customers around the world.
We are 6000 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