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 language | English |
---|---|
Title of host publication | IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015 |
Place of Publication | Los Alamitos |
Publisher | IEEE |
Pages | 139-148 |
Number of pages | 10 |
Volume | 2 |
ISBN (Print) | 978-1-4799-1934-5 |
DOIs | |
Publication status | Published - May 2015 |
Event | 37th IEEE International Conference on Software Engineering 2015 - Florence, Italy Duration: 16 May 2015 → 24 May 2015 |
Conference
Conference | 37th IEEE International Conference on Software Engineering 2015 |
---|---|
Abbreviated title | ICSE 2015 |
Country/Territory | Italy |
City | Florence |
Period | 16/05/15 → 24/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.Profiles
-
Manuel Maarek
- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor
Person: Academic (Research & Teaching)