Practical application of SPARK: a business case and roadmap for new users

Stuart Matthews - Altran UK

The range of options available when applying SPARK can be daunting for users who are new to the field of formal methods and static verification. More recently Altran UK have mapped our experience on previous projects into a framework (co-developed with AdaCore and Thales) which is intended to provide new users with a roadmap for navigating their way to obtaining optimum value from using SPARK. The details of how SPARK should be applied depends on multiple factors which include the required integrity level, applicable standards, and the overall verification strategy for the system. Far from being academic, theoretical or an idealistic vision, we demonstrate a highly pragmatic approach which is not only demonstrably beneficial but also accessible and practicable by developers who are new to the application of formal methods. As well as presenting the framework and its historical context, this talk will reflect on the wider business case and commercial implications for the application of SPARK within an organisation such as Altran which is responsible for delivering high integrity systems.

Download this presentation

About Stuart Matthews

Stuart Matthews has over 20 years' experience with high integrity software engineering and technology management. Stuart is currently the R&T Manager within the Intelligent Systems Expertise Centre at Altran UK with responsibility for the technology pipeline and a portfolio of on-going research projects. The portfolio includes the SPARK technology & support services for which Stuart also acts as the product manager at Altran.