Improving Predictability, Efficiency and Trust of Model-Based Proof Activity

Jean-Frederic Etienne, Manuel Maarek, Florent Anseaume, Veronique Delebarre

Research output: Chapter in Book/Report/Conference proceedingConference contribution

82 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publication IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015
Place of PublicationLos Alamitos
PublisherIEEE
Pages139-148
Number of pages10
Volume2
ISBN (Print)978-1-4799-1934-5
DOIs
Publication statusPublished - May 2015
Event37th IEEE International Conference on Software Engineering 2015 - Florence, Italy
Duration: 16 May 201524 May 2015

Conference

Conference37th IEEE International Conference on Software Engineering 2015
Abbreviated titleICSE 2015
Country/TerritoryItaly
CityFlorence
Period16/05/1524/05/15

Fingerprint

Dive into the research topics of 'Improving Predictability, Efficiency and Trust of Model-Based Proof Activity'. Together they form a unique fingerprint.

Cite this