Проектируем по спецификации. Часть 2
Конечно, в повседневной Android разработке применение формальных методов верификации является дорогим удовольствием и вообще не используется. Однако, в крупных компаниях у нас есть не только продуктовые команды, но и технические. Есть команды инфраструктуры, отвечающие за процессы разработки и качество жизни всех разработчиков в команде. Также мне встречались команды RnD, занимающиеся совсем глубокими техническими исследованиями и экспериментами.
Принимая во внимание тот факт, что типичный проект состоит из некоторой core части, где написанный код должен быть максимально надежным, оптимальным и поддерживаемым, то почему бы не ввести правило, что написанный в core части код должен обладать спецификацией, должен следовать правильным методикам ООП и быть верифицированным, хотя бы с использованием неформального подхода? Рассмотренная в предыдущей статье задача про локальное хранилище токенов как раз относится к этому.
Также частый сценарий, который требуется сделать в клиент-серверном приложении, это обновление токена авторизации. Никогда не приходилось встречать наличие спецификаций этого процесса. Так, вопросы типа “Перезапрос токена”, “Очередь потоков на обновление”, “Обрабатываемые/необрабатываемые ошибки” (как на прикладном уровне, так и на бизнес уровне), “защита от ddos сервера” и т.д. остаются нераскрытыми и по-сути отдаются на откуп разработчику. А когда этот разработчик, например, увольняется, то понимание “как это должно работать” переходит уже к другому человеку. Разработчики имеют привычку рассуждать о работе компонента не в понимании “Как оно должно работать согласно аналитики”, а “Как оно сделано”. В итоге, полный рассинхрон между командами разработки и менеджерами.
В рамках текущей статьи рассмотрим формальный подход, который в типичных Android проектах не используется, да и на самом деле неприменим по причинам, указанным ниже. И далее рассмотрим уже неформальные подходы.
Формальная логика в программировании позволяет разработчикам точно описывать и анализировать поведение программных систем. Есть различные инструменты для этих задач, рассмотрим несколько.
Инструменты для формальной верификации спецификаций
Формальная верификация - это процесс использования математических методов проверки для утверждения правильности системы относительно определенной спецификации или свойства. В программной инженерии это означает доказательство, что программа делает то, что от неё ожидают. И не делает того, чего от нее не ожидают. Для этого используются различные инструменты, которые здесь кратко описаны:
Модельные проверяющие (Model Checkers): Инструменты типа SPIN или Promela, которые могут автоматически анализировать выполнимые модели систем. Они эффективно перебирают все возможные состояния системы для проверки, удовлетворяет ли система определенным требованиям безопасности или другим свойствам.
Доказательства теорем (Theorem Provers): Инструменты вроде Coq, HOL (Higher-order logic) или Isabelle, которые позволяют пользователям формулировать спецификации и доказательства в виде математических теорем. Они требуют глубокого понимания логики и большого объема работы вручную, но позволяют достигать высокого уровня достоверности верификации.
SAT и SMT решатели: Системы, которые используются для решения задач высказываний и формул первого порядка (SAT для Boolean-выражений и SMT для более сложных логических формул). Примеры включают Z3 от Microsoft Research. Эти инструменты широко применяются для решения ограничений в автоматической верификации и синтезе программ.
Спецификация и верификация программного обеспечения: Инструменты как Alloy, использующийся для моделирования структур и их взаимодействий в программном обеспечении перед реальной реализацией, чтобы проверить логическую подоплеку дизайна.
Общий пример применения методов формальной верификации
Задача: Спроектировать на основе SharedPreferences локальное хранилище токенов авторизации в Android приложении с использованием инструментов формальной верификации.
Шаг 1: Спецификация требований
Для начала определим требования к нашему локальному хранилищу токенов:
- Сохранение токена: Система должна предоставлять возможность сохранять токен авторизации.
- Чтение токена: Система должна предоставлять возможность извлекать сохраненный токен.
- Удаление токена: Система должна предоставлять возможность удалять сохраненный токен.
- Безопасность: Токены не должны быть доступны для других приложений на устройстве и должны храниться в криптостойком хранилище.
Шаг 2: Моделирование и анализ
Используем инструмент моделирования (например, Alloy) для создания абстрактной модели хранилища. Моделирование включает в себя определение сущностей (токенов) и операций (сохранение, чтение, удаление).
На основании этой модели проводим анализ, используя методы формальной верификации для проверки соответствия модели нашим требованиям безопасности и функциональности.
Шаг 3: Реализация и тестирование
Основываясь на верифицированной спецификации, переходим к реализации хранилища на Android с использованием SharedPreferences. Реализация включает разработку соответствующих методов для сохранения, извлечения и удаления токенов, а также обеспечение их безопасности.
После реализации проводим тестирование, используя юнит-тесты, чтобы проверить соответствие реализации изначальной спецификации и требованиям.
Подробный пример применения методов формальной верификации
Документ, в котором описывается применение методов верификации модели разрешений (permissions) в Android с математическими выкладками: Формальный подход к верификации модели разрешений в Android
Выводы
Теперь рассмотрим причины, почему ждать применения таких инженерных подходов в коммерческих проектах не стоит, по крайней мере в обозримом будущем.
Высокая стоимость внедрения. Формальная верификация требует значительных начальных инвестиций, как в плане времени, так и средств. Необходимо не только создать полную и безошибочную спецификацию всех аспектов приложения, но и иметь специалистов, владеющих необходимыми навыками для работы с инструментами формальной верификации. Подобные эксперты ценятся высоко, а их обучение может быть длительным и сложным процессом.
Сложность применения. Многие техники и инструменты формальной верификации обладают высокой степенью сложности и предназначены для моделирования и анализа на абстрактном уровне, что может оказаться нецелесообразным для многих коммерческих приложений. Перевод требований повседневных Android-приложений в строгие формальные спецификации также представляет собой непростую задачу.
Время разработки. Использование формальных методов значительно увеличивает время разработки проектов. В условиях строгих крайних сроков и постоянно меняющихся требований бизнеса время разработки становится критическим ресурсом. Предпочтение отдается тем методологиям разработки, которые позволяют быстро производить итерации и адаптироваться к изменениям.
На этом обзор методов формального подхода к проектированию завершен, далее рассмотрим то, что в целом применимо к мейнстримной, коммерческой разработке: неформальные методы верификации программных систем. Могут ли они быть полезными и улучшают ли они здоровье проекта.