maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2019-4-520-533mais-1274Research ArticleComputing Methodologies and ApplicationsДоказательство свойств дискретных функций с помощью дедуктивного доказательства: приложение к квадратному корнюProving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Roothttps://orcid.org/0000-0002-2739-499XТодоровВасилTodorovVassilvassil.todorov@lri.frhttps://orcid.org/0000-0003-3950-6415ТахаСафуанTahaSafouan

PhD

PhD

safouan.taha@lri.frhttps://orcid.org/0000-0003-3185-2807БуланжеФредерикBoulangerFrederic

PhD

frederic.boulanger@lri.frhttps://orcid.org/0000-0003-4555-4616ЭрнандесАрмандоHernandezArmandoarmando.hernandez@mpsa.comGroupe PSAФранцияGroupe PSAFranceCentraleSupelecФранцияCentraleSupelecFrance201913122019264520533Copyright © Тодоров В., Таха С., Буланже Ф., Эрнандес А., 20192019Тодоров В., Таха С., Буланже Ф., Эрнандес А.Todorov V., Taha S., Boulanger F., Hernandez A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1274

В течение многих лет автомобильные встраиваемые системы проверялись только тестированием. В ближайшем будущем усовершенствованные системы помощи водителю (ADAS) будут играть большую роль в дизайне и разработке программного обеспечения автомобиля. Кроме того, увеличение их критического уровня может привести к тому, что власти потребуют сертификации этих систем. Мы думаем, что привнесение формальных доказательств в их развитие может помочь обеспечить выполнение свойств безопасности и получить эффективный процесс сертификации. Другие отрасли (например, аэрокосмическая, железнодорожная, ядерная), которые создают критические системы, требующие сертификации, также могут быть заинтересованы в развитии формальных методов проверки. Одним из этих методов является дедуктивное доказательство. Это может дать более высокий уровень уверенности в доказательстве критических свойств безопасности и даже избежать модульное тестирование. В этой статье мы выбрали вариант прикладного использования: функцию, вычисляющую квадратный корень с помощью линейной интерполяции. Мы используем дедуктивное доказательство, чтобы доказать его правильность и показать ограничения, с которыми мы сталкиваемся при работе с готовыми инструментами. Мы предлагаем подходы для преодоления некоторых ограничений, связанных с этими инструментами, чтобы преуспеть с доказательством. Эти подходы могут быть применены к аналогичным проблемам, которые часто встречаются в автомобильном встроенном программном обеспечении.

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.

формальные методыдедуктивное доказательстводоказательство дискретных функцийformal methodsdeductive proofproving discrete-valued functionsЭта работа была поддержана Groupe PSA, французским многонациональным производителем автомобилей и мотоциклов, которые продаются под брендами Peugeot, Citro¨en, DS, Opel и Vauxhall.This work was supported by the Groupe PSA, a French multinational manufacturer of automobiles and motorcycles sold under the Peugeot, Citro¨en, DS, Opel and Vauxhall brands.ReferencesAagaard M. D., Jones R. B., Kaivola R., Kohatsu K. R., Seger C.-J. H., “Formal Verification of Iterative Algorithms in Microprocessors”, Proceedings of the 37th Annual Design Automation Conference (DAC 2000), 2000, 201–206.Aagaard M. D., Jones R. B., Kaivola R., Kohatsu K. R., Seger C.-J. H., “Formal Verification of Iterative Algorithms in Microprocessors”, Proceedings of the 37th Annual Design Automation Conference (DAC 2000), 2000, 201–206.Hoare A., Chapron P., Abrial J. R., The B-book: Assigning Programs to Meanings, Cambridge University Press, New York, NY, USA, 1996.Hoare A., Chapron P., Abrial J. R., The B-book: Assigning Programs to Meanings, Cambridge University Press, New York, NY, USA, 1996.Barnett M., Leino K. R. M., “Weakest-Precondition of Unstructured Programs”, Softw. Eng. Notes, 31:1 (2005), 82–87.Barnett M., Leino K. R. M., “Weakest-Precondition of Unstructured Programs”, Softw. Eng. Notes, 31:1 (2005), 82–87.Barrett C., Conway C. L., Deters M., Hadarean L., Jovanovi’c D., King T., Reynolds A., Tinelli C., “Cvc4.”, Computer Aided Verification. CAV 2011. LNCS, 6806 (2011), 171–177.Barrett C., Conway C. L., Deters M., Hadarean L., Jovanovi’c D., King T., Reynolds A., Tinelli C., “Cvc4.”, Computer Aided Verification. CAV 2011. LNCS, 6806 (2011), 171–177.Barrett C. et al., “The SMT-LIB Standard: Version 2.0.”, Tech. rep., 2010.Barrett C. et al., “The SMT-LIB Standard: Version 2.0.”, Tech. rep., 2010.Bertot Y., Magaud N., Zimmermann P., “A Proof of GMP Square Root”, Journal of Automated Reasoning, 29:3-4 (2002), 225–252.Bertot Y., Magaud N., Zimmermann P., “A Proof of GMP Square Root”, Journal of Automated Reasoning, 29:3-4 (2002), 225–252.Chapman R., “Industrial Experience with SPARK”, ACM SIGAda Ada Letters, 20:4 (2000), 64–68.Chapman R., “Industrial Experience with SPARK”, ACM SIGAda Ada Letters, 20:4 (2000), 64–68.Conchon S., Coquereau A., Iguernlala M., Mebsout A., “Alt-Ergo 2.2”, SMT Workshop: International Workshop on SMT. Oxford, United Kingdom, 2018.Conchon S., Coquereau A., Iguernlala M., Mebsout A., “Alt-Ergo 2.2”, SMT Workshop: International Workshop on SMT. Oxford, United Kingdom, 2018.De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, TACAS’08/ETAPS’08, SpringerVerlag, Berlin, Heidelberg, 4963 (2008), 337–340.De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, TACAS’08/ETAPS’08, SpringerVerlag, Berlin, Heidelberg, 4963 (2008), 337–340.Dijkstra E.W., “Guarded Commands, Nondeterminacy and Formal Derivation of Programs”, ACM, 18:8 (1975), 453–457.Dijkstra E.W., “Guarded Commands, Nondeterminacy and Formal Derivation of Programs”, ACM, 18:8 (1975), 453–457.Dutertre B., “Yices 2.2”, International Conference on Computer Aided Verification. Springer, Cham, 2014, 737–744.Dutertre B., “Yices 2.2”, International Conference on Computer Aided Verification. Springer, Cham, 2014, 737–744.Ferguson W. E., Bingham J., Erk¨ok L., Harrison J. R., Leslie-Hurd J., “Digit Serial Methods with Applications to Division and Square Root”, IEEE Transactions on Computers, 67:3 (2017), 449–456.Ferguson W. E., Bingham J., Erk¨ok L., Harrison J. R., Leslie-Hurd J., “Digit Serial Methods with Applications to Division and Square Root”, IEEE Transactions on Computers, 67:3 (2017), 449–456.Flanagan C., Flanagan C., Saxe J. B., “Avoiding Exponential Explosion: Generating Compact Verification Conditions”, ACM SIGPLAN Not., 36:3 (2001), 193–205.Flanagan C., Flanagan C., Saxe J. B., “Avoiding Exponential Explosion: Generating Compact Verification Conditions”, ACM SIGPLAN Not., 36:3 (2001), 193–205.Harrison J., “Formal Verification of Square Root Algorithms”, Formal Methods in System Design, 22:2 (2003), 143–153.Harrison J., “Formal Verification of Square Root Algorithms”, Formal Methods in System Design, 22:2 (2003), 143–153.Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12:10 (1969), 576–580.Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12:10 (1969), 576–580.Kirchner F., Kosmatov N., Prevosto V., Signoles J., Yakobowski B., “Frama-C: A Software Analysis Perspective”, Formal Aspects of Computing, 27:3 (2015), 573–609.Kirchner F., Kosmatov N., Prevosto V., Signoles J., Yakobowski B., “Frama-C: A Software Analysis Perspective”, Formal Aspects of Computing, 27:3 (2015), 573–609.Kuliamin V. V., “Standardization and Testing of Implementations of Mathematical Functions in Floating Point Numbers”, Programming and Computer Software, 33:3 (2007), 154–173.Kuliamin V. V., “Standardization and Testing of Implementations of Mathematical Functions in Floating Point Numbers”, Programming and Computer Software, 33:3 (2007), 154–173.Mauborgne L., “Astr´ee: Verification of Absence of Runtime Error”, In: Jacquart R. (eds) Building the Information Society. IFIP International Federation for Information Processing, 156 (2004), 385–392.Mauborgne L., “Astr´ee: Verification of Absence of Runtime Error”, In: Jacquart R. (eds) Building the Information Society. IFIP International Federation for Information Processing, 156 (2004), 385–392.Melquiond G., Rieu-Helft R., “Formal Verification of a State-of-the-Art Integer Square Root”, IEEE 26th Symposium on Computer Arithmetic (ARITH), Kyoto, Japan, 2019, 183–186.Melquiond G., Rieu-Helft R., “Formal Verification of a State-of-the-Art Integer Square Root”, IEEE 26th Symposium on Computer Arithmetic (ARITH), Kyoto, Japan, 2019, 183–186.Moy Y., Ledinot E., Delseny H., Wiels V., Monate B., “Testing or Formal Verification: DO-178C Alternatives and Industrial Experience”, IEEE Soft, 30:3 (2013), 50-57.Moy Y., Ledinot E., Delseny H., Wiels V., Monate B., “Testing or Formal Verification: DO-178C Alternatives and Industrial Experience”, IEEE Soft, 30:3 (2013), 50-57.Rager D. L., Ebergen J., Nadezhin D., Lee A., Chau C. K., Selfridge B., “Formal Verification of Division and Square Root Implementations, an Oracle Report.”, Formal Methods in Computer-Aided Design (FMCAD), 2016, 149–152.Rager D. L., Ebergen J., Nadezhin D., Lee A., Chau C. K., Selfridge B., “Formal Verification of Division and Square Root Implementations, an Oracle Report.”, Formal Methods in Computer-Aided Design (FMCAD), 2016, 149–152.Randimbivololona F., Souyris J., Baudin P., Pacalet A., Raguideau J., Schoen D., “Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach”, In: Wing J. M., Woodcock J., Davies J. (eds) — Formal Methods. FM 1999, 1709 (1999), 1798–1815.Randimbivololona F., Souyris J., Baudin P., Pacalet A., Raguideau J., Schoen D., “Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach”, In: Wing J. M., Woodcock J., Davies J. (eds) — Formal Methods. FM 1999, 1709 (1999), 1798–1815.Russinoff D. M., “A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode”, Formal Methods in System Design, 14:1 (1999), 75–125.Russinoff D. M., “A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode”, Formal Methods in System Design, 14:1 (1999), 75–125.Russinoff D. M., “A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7TM Processor”, LMS J. Comput. Math. (UK), 1 (1998), 148–200.Russinoff D. M., “A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7TM Processor”, LMS J. Comput. Math. (UK), 1 (1998), 148–200.Sawada J., Gamboa R., “Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem”, LNCS. Formal Methods in Computer-Aided Design. FMCAD 2002., 2517 (2002), 274–291.Sawada J., Gamboa R., “Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem”, LNCS. Formal Methods in Computer-Aided Design. FMCAD 2002., 2517 (2002), 274–291.Shelekhov V. I., “Verification and Synthesis of Addition Programs under the Rules of Correctness of Statements”, Automatic Control and Computer Sciences, 45:7 (2011), 421–427.Shelekhov V. I., “Verification and Synthesis of Addition Programs under the Rules of Correctness of Statements”, Automatic Control and Computer Sciences, 45:7 (2011), 421–427.Shilov N. V., Anureev I. S., Bodin E. V., “Generation of Correctness Conditions for Imperative Programs”, Programming and Computer Software, 34:6 (2008), 307–321.Shilov N. V., Anureev I. S., Bodin E. V., “Generation of Correctness Conditions for Imperative Programs”, Programming and Computer Software, 34:6 (2008), 307–321.Шилов Н. В., Кондратьев Д. А., Ануреев И. С., Бодин Е. В., Промский А. В., “Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня”, Моделирование и анализ информационных систем, 25:6 (2018), 637-666.Shilov N. V., Kondratyev D. A., Anureev I. S., Bodin E. V., Promsky A. V., “Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function”, Modeling and Analysis of Information Systems, 25:6 (2018), 637-666, (in Russian).Todorov V., Boulanger F., Taha S., “Formal Verification of Automotive Embedded Software”, Proceedings of the 6th Conference on Formal Methods in Software Engineering. ACM, New York, USA, 2018, 84–87.Todorov V., Boulanger F., Taha S., “Formal Verification of Automotive Embedded Software”, Proceedings of the 6th Conference on Formal Methods in Software Engineering. ACM, New York, USA, 2018, 84–87.

The authors declare that there are no conflicts of interest present.