Что такое программное обеспечение, критичное к безопасности, и как Ada и SPARK могут помочь?

12 февр. 2019 г. автор: Жан-Пьер Розен FOSDEM, 2019 Мы слишком часто имеем дело с ошибочным кодом имеющим различной степени последствия и привыкли к тому, что ошибки в программном обеспечении - неизбежная участь. Но для критически важного для безопасности программного обеспечения, который управляет самолетами или поездами, должен быть код выполняющий требование "Отказ невозможен". В этой презентации рассказывается об ограничениях такого программного обеспечения и о том, что они требуют особого подхода, специальных методов и специальных инструментов, таких как Ada и SPARK. И это может быть полезно для более повседневного программирования - программное обеспечение с нулевыми ошибками прекрасно, даже если оно не критично для безопасности!