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

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

doi:10.1109/ICSE.2015.142

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

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

SafeRiver

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1109/ICSE.2015.142
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

Access to Document

10.1109/ICSE.2015.142

Download pdf
© 2016 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Accepted author manuscript, 332 KBLicence: Copyright Publisher

Manuel Maarek
- M.Maarekhw.acuk
- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor
Person: Academic (Research & Teaching)

Cite this

@inproceedings{329eb3e39fd24f5cbae375b728bdaa86,

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

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.",

author = "Jean-Frederic Etienne and Manuel Maarek and Florent Anseaume and Veronique Delebarre",

year = "2015",

month = may,

doi = "10.1109/ICSE.2015.142",

language = "English",

isbn = "978-1-4799-1934-5",

volume = "2",

pages = "139--148",

booktitle = "IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015",

publisher = "IEEE",

address = "United States",

note = "37th IEEE International Conference on Software Engineering 2015, ICSE 2015 ; Conference date: 16-05-2015 Through 24-05-2015",

}

Etienne, J-F, Maarek, M, Anseaume, F & Delebarre, V 2015, Improving Predictability, Efficiency and Trust of Model-Based Proof Activity. in IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015. vol. 2, IEEE, Los Alamitos, pp. 139-148, 37th IEEE International Conference on Software Engineering 2015, Florence, Italy, 16/05/15. https://doi.org/10.1109/ICSE.2015.142

TY - GEN

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

AU - Etienne, Jean-Frederic

AU - Maarek, Manuel

AU - Anseaume, Florent

AU - Delebarre, Veronique

PY - 2015/5

Y1 - 2015/5

N2 - 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.

AB - 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.

U2 - 10.1109/ICSE.2015.142

DO - 10.1109/ICSE.2015.142

M3 - Conference contribution

SN - 978-1-4799-1934-5

VL - 2

SP - 139

EP - 148

BT - IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), 2015

PB - IEEE

CY - Los Alamitos

T2 - 37th IEEE International Conference on Software Engineering 2015

Y2 - 16 May 2015 through 24 May 2015

ER -

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

Abstract

Conference

Access to Document

Fingerprint

Profiles

Manuel Maarek

Cite this