Geodesic
Proving properties of discrete-valued functions using deductive proof: application to the square root
Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 520-533

Voir la notice de l'article provenant de la source Math-Net.Ru

For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is deductive proof. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing. In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in the automotive embedded software.
Keywords: formal methods, deductive proof, proving discrete-valued functions. 
@article{MAIS_2019_26_4_a4,
     author = {V. Todorov and S. Taha and F. Boulanger and A. Hernandez},
     title = {Proving properties of discrete-valued functions using deductive proof: application to the square root},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {520--533},
     publisher = {mathdoc},
     volume = {26},
     number = {4},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a4/}
}
TY  - JOUR
AU  - V. Todorov
AU  - S. Taha
AU  - F. Boulanger
AU  - A. Hernandez
TI  - Proving properties of discrete-valued functions using deductive proof: application to the square root
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2019
SP  - 520
EP  - 533
VL  - 26
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a4/
LA  - en
ID  - MAIS_2019_26_4_a4
ER  - 
%0 Journal Article
%A V. Todorov
%A S. Taha
%A F. Boulanger
%A A. Hernandez
%T Proving properties of discrete-valued functions using deductive proof: application to the square root
%J Modelirovanie i analiz informacionnyh sistem
%D 2019
%P 520-533
%V 26
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a4/
%G en
%F MAIS_2019_26_4_a4
V. Todorov; S. Taha; F. Boulanger; A. Hernandez. Proving properties of discrete-valued functions using deductive proof: application to the square root. Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 520-533. http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a4/