Plenary Talks
B+ or how to model system properties in a formal software model
Software development for mission-critical applications requires a level of confidence that can be achieved through the use of formal methods. For a number of industrial applications, there is a lack of high-level properties to be verified, and proof mainly replaces unit testing. This talk presents an integrated approach based on more than 20 years of industrial practice, which enables so-called “system” properties to be modelled in a formal software model. The proof of the system’s safety is not carried out entirely formally, but it is entirely guided by the model. It is based on 2 principles which are illustrated by means of a demonstrative example.