Мадрид (июнь-2015)

[kornevgen]

Пишу этот текст по просьбе моего замечательного приятеля, коллеги Виталия Брагилевского, знакомство с которым произошло тоже в заграничной поездке.

В этот раз мы с коллегами по ИСП РАН съездили в Мадрид на мероприятия, посвященные архитектурному моделированию при помощи языка AADL. Они проходили в рамках конференции Ada-Europe 2015. Мы были в

Comments

[kornevgen]

Можно :-) Мне хватило иллюстраций на слайдах :-) Кстати, вся доска в несколько раз больше, чем кусочек на фото.

Я рассказывал про предлагаемый нами подход к одному из видов верификации моделей программно-аппаратных систем, разработанных на языке моделирования AADL. Под верификацией понимается очень простая штука, формулирование проверяемых ограничений и их выполнение на модели. Формализм ограничений тоже довольно простой, потому что всё это делается для обычных инженеров - системных интеграторов (это которые собирают из готовых компонентов системы для авионики, т.е. авиационную электронику), даже не обладающих математическим и программистским бэкграундом, но готовых обучаться чему-то полезному. Формализм был предложен 5 лет назад, а борьба идет за то, как подать его так, чтобы от него не отвернулись эти инженеры и могли им пользоваться. Поэтому в формализме нет каких-либо намеков на логику предикатов, кванторы и т.п. Собственно, идея AADL состоит и в том, чтобы предложить небольшой набор типовых компонентов и несколько механизмов их расширения и комбинирования для получения моделей программно-аппаратных систем на разных уровнях абстракции и начинать автоматизированный анализ этих моделей на как можно более абстрактных моделях. Абстрактность получается тогда, когда мы вместо некоторой части (которую еще не спроектировали) ставим компонент типа "нечто" и задаем, какими "атрибутами" будет обладать это "нечто"; этого уже бывает достаточно, чтобы провести некоторый анализ модели и, возможно, найти ошибки, например, несовместимый набор атрибутов некоторых компонентов, уже помещенных в систему.
Так вот, возвращаясь к верификации. Заморские коллеги предлагают инженерам специально созданные новые языки, на которых инженеры должны формулировать ограничения к структуре модели. Мы предлагаем "не выдумывать колесо", а взять готовый язык программирования и на нем записывать ограничения. Плюс в том, что нам не нужно самим разрабатывать и поддерживать компиляторы/интерпретаторы и всякие умные редакторы - они уже есть, причем вполне достойного качества. Например, уже есть редактор с раскраской кода, автопродолжением и многим другим, а среды разработки уже имеют отладчик. Заморским коллегам приходится всё это разрабатывать самим, плюс придумывая заковыристые языки, которые не хотят осваивать инженеры. Еще один плюс в том, что наши инженеры могут переиспользовать готовый код на этом языке программирования (в частности, реализацию многих полезных структур данных), а заморским коллегам приходится всё это включать в свой язык записи ограничений, от чего он ставится еще сложнее.

Среди публики был один из авторов альтернативного подхода. Он задал вопрос, ответ на который его удовлетворил: он спросил, когда обнаруживается ошибка в ограничениях в нашем подходе. Она обнаружится, только при попытке выполнить исходный код ограничения. А в его подходе он пишет сам дополнительно семантический анализатор и ошибку находит и подсвечивает еще при написании текста ограничения. Мои коллеги сказали, что это он вставит в свою следующую статью, описывая преимущества своего подхода над нашим :-) Еще были вопросы на тему того, действительно ли наши инженеры согласны использовать языки программирования. И, таки, да, именно поэтому мы и разрабатываем свой подход.