We report on our industrial experience in using formal methods for the analysis of safety-critical systems developed in a model-based design framework. We first highlight the formal proof workflow devised for the verification and validation of embedded systems developed in Matlab/Simulink. In particular, we show that there is a need to: determine the compatibility of the model to be analysed with the proof engine, establish whether the model facilitates proof convergence or when optimisation is required, and avoid over-specification when specifying the hypotheses constraining the inputs of the model during analysis. We also stress on the importance of having a certain harness over the proof activity and present a set of tools we developed to achieve this purpose. Finally, we give a list of best practices, methods and any necessary tools aiming at guaranteeing the validity of the verification results obtained.
|Title of host publication||IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015|
|Place of Publication||Los Alamitos|
|Number of pages||10|
|Publication status||Published - May 2015|
|Event||37th IEEE International Conference on Software Engineering 2015 - Florence, Italy|
Duration: 16 May 2015 → 24 May 2015
|Conference||37th IEEE International Conference on Software Engineering 2015|
|Abbreviated title||ICSE 2015|
|Period||16/05/15 → 24/05/15|
FingerprintDive into the research topics of 'Improving Predictability, Efficiency and Trust of Model-Based Proof Activity'. Together they form a unique fingerprint.
- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor
Person: Academic (Research & Teaching)