Proving properties of discrete-valued functions using deductive proof: application to the square root

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