Лекция 1. История вопроса и текущее состояние проблемы

• когда и как пытались строго описывать программы и/или программные системы
• в чем разница между программой и программной системой
• первая трактовка √ это чисто количественное различие (размер и сложность)
• вторая трактовка:
• программа √ это разные представления (исходный текст, блок-схема, структура потокв данных и проч)
• система √ это назначение, функциональность, поведение, способы использования
• Ю.Янов √ описание программы, IBM Input/Output charts √ описание системы
• Языки программирования, IBM flow chart √ описание программы,
• Языки спецификаций √ описание системы
• Мечта об автоматической генерации ПО
• Замечание: средства программирования (инструменты) лет 20-30 назад обычно назывались средствами автоматизации программирования
• Описать требования, описать вычислитель, сгенерировать программу для вычислителя.
• Итоги:
• Некоторые этапы были автоматизированы √ трансляция, линковка, загрузка, из новых √ сборка конфигураций, автоматизированный сбор изменений и их описаний и др.
• Осознаны две основные проблемы:
• как описать требования к (свойствам, функциональности) системы
• нотации и методы
• критерии правильности и способы проверки правильности требований
• как перейти от описаний свойств к их алгоритмам, то есть к способу достижения этих свойств
• Наиболее известный пример удачного использований √ VDM/ADA компилятор
• Другие успехи:
• Генерация парсеров по описанию языка
• Построение СУБД по описанию схемы
• Построение пользовательских интерфейсов по описанию диалогов
• Вывод √ удается эффективно использовать формализмы в специализированных приложениях и не удается построить универсальную технологию, где отталкиваясь от формального описания (автоматически) удается получить готовую программу.
• Другие способы использования формальных методов.
• (Автоматическая) проверка правильности программ (верификация и валидация) и аппаратуры
• Анализ проектных решений (для программ и апаратуры)
• Анализ бизнес процессов
• Общее видение места формальных методов в разработке ПО
• ФМ √ инструмент для (облегчения) анализа как готовых программ/устройств/процессов
• Для облегчения анализа требуется
• абстрагироваться от деталей √ строить упрощенные (логические) модели
• одной и той же сущности могут соответствовать разные модели, поскольку
• разные аспекты абстрагирования √ от чего мы отвлекаемся и что оставляем в кругу рассмотрения
• разные формализмы (конечные автоматы, грамматики, графы, исчисления) и нотации (графические, текстовые)
• сопоставлять модели между собой (рассматривая реализации, как частный случай моделей)
• статические виды анализа (сравниваются программы и/или спецификации)
• динамические виды анализа (сравниваются поведения систем и моделей)
• трансформировать одни модели в другие
• порождать (генерировать) одни описания/спецификации/программы на основе других, наприммер
• из требований порождать тестовые воздействия, сценарии тестирования и критерии проверки правильности
• из сценариев использования (описания поведения пользоввателя) генерировать реализацию и тесты
• из спецификации (реализации) генерировать документацию (по использованию) и т.д.
• Тем самым √ ФМ это инструмент для моделирования систем и их проектов и реализаций.
• Крайне важно усвоить отношение к спецификации как модели, поскольку каждый раз, изучив свойства модели, мы не должны забывать о вопросе соответствия данной модели и реальной системы.
• Нет никаких полных методов определения корректности системы за исключением экспериментальной проверки, сопоставления реализации с моделями, использованными для описания требований или ожидаемых свойств. Д.Бьорнер √ Formal specification is an experimental science.
• Модели должны быть формальны, поскольку только такие модели могут использоваться/анализироваться/трансформироваться машиной.
• Для систем реальной сложности не существует одного вида моделей, которые исчерпывающим образом отвечают всем требованиям анализа системы => необходимы разные подходы к моделированию и разные уровни детализации в рамках каждго из видов.