Reducing the Cost of Software Using Scalable Model-Based Formal Verification
Today's products in many sectors, such as aerospace, automotive, medical, and high-tech manufacturing, depend increasingly on software to function. This software is becoming increasingly complex and development costs are escalating. At the same time, there is continued pressure to reduce time-to-market and reduce delivered defects. In many cases, the increase in complexity means that conventional testing practices are falling short by failing to guarantee the necessary software quality and contributing to escalating development costs. Unlike testing, formal verification is able to automatically analyse the system in all possible scenarios and can therefore guarantee the absence of errors.
In this presentation, we will give an overview of how one can tackle the challenge of escalating software costs by enhancing model-based engineering platforms with fully automated, scalable, formal verification technologies combined with automatic code generation. The advantages of our approach include: finding and fixing design errors earlier in the development cycle; increasing the reliability of the resulting software; increasing the reusability of components; supporting parallel development; and improving time-to-market by reducing the possibility of integration errors. This work is being carried out as part of several large research projects at the University of Oxford, and builds on theory, technology and experience that has been developed within this group over several decades.