Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root
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 certifi...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2019-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1274 |
| _version_ | 1797877912775426048 |
|---|---|
| author | Vassil Todorov Safouan Taha Frederic Boulanger Armando Hernandez |
| author_facet | Vassil Todorov Safouan Taha Frederic Boulanger Armando Hernandez |
| author_sort | Vassil Todorov |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:24:25Z |
| format | Article |
| id | doaj.art-e71d5ec5d9344c4bba29b7852ea27b7b |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:25Z |
| publishDate | 2019-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-e71d5ec5d9344c4bba29b7852ea27b7b2023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172019-12-0126452053310.18255/1818-1015-2019-4-520-533951Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square RootVassil Todorov0Safouan Taha1Frederic Boulanger2Armando Hernandez3Groupe PSACentraleSupelecCentraleSupelecGroupe PSAFor 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.https://www.mais-journal.ru/jour/article/view/1274формальные методыдедуктивное доказательстводоказательство дискретных функций |
| spellingShingle | Vassil Todorov Safouan Taha Frederic Boulanger Armando Hernandez Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root Моделирование и анализ информационных систем формальные методы дедуктивное доказательство доказательство дискретных функций |
| title | Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root |
| title_full | Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root |
| title_fullStr | Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root |
| title_full_unstemmed | Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root |
| title_short | Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root |
| title_sort | proving properties of discrete valued functions using deductive proof application to the square root |
| topic | формальные методы дедуктивное доказательство доказательство дискретных функций |
| url | https://www.mais-journal.ru/jour/article/view/1274 |
| work_keys_str_mv | AT vassiltodorov provingpropertiesofdiscretevaluedfunctionsusingdeductiveproofapplicationtothesquareroot AT safouantaha provingpropertiesofdiscretevaluedfunctionsusingdeductiveproofapplicationtothesquareroot AT fredericboulanger provingpropertiesofdiscretevaluedfunctionsusingdeductiveproofapplicationtothesquareroot AT armandohernandez provingpropertiesofdiscretevaluedfunctionsusingdeductiveproofapplicationtothesquareroot |