Организация вычислений в компонентах. 3 страница

Заметим далее в строке 31, что pthread_cond_wait принимает в качестве аргумента &mutex. Пока поток блокируется на ожидании, он временно освобождает замок мутекса. Если не сделать этого, тогда поток producer не сможет попасть в критическую секцию и, следовательно, не сможет послать сообщение. Программа окажется в состоянии взаимоблокировки. Перед выходом из pthread_cond_wait, функция будет вновь получать замок мутекса. Программист должен быть очень аккуратным, когда вызывает pthread_cond_wait, т.к. замок мутекса временно освобожден во время вызова. Заметим что, значение некоторой разделяемой переменной после вызова pthread_cond_wait может быть отличным от значения до вызова.

Условные переменные, использованные в предыдущем примере, есть обобщенная форма семафоров. Программные семафоры получили свое название вслед механическим сигналам, традиционно используемым на железнодорожных путях для сигнализации о том, что на перегоне пути присутствует состав. Использование таких семафоров сделало возможным движение по одной колее в двух направлениях (семафор реализует взаимное исключение, препятствующее одновременному движению двум составом по одному участку пути).

В 60-е годы прошлого века Е. Дейкстра заимствовал эту идею, чтобы показать, как программы могут надежно разделять ресурсы. Вычислительный семафор (PV семафор Дейкстра) это неотрицательная целая (натуральная) переменная. Значение 0 рассматривается обособленно. Фактически переменная size из предыдущего примера является семафором. Она увеличивается при отправке сообщений, а величина 0 блокирует consumer, пока значение станет ненулевым. Переменная условия обобщает эту идею, поддерживая произвольные условия, а не только 0 или не 0, как критерий для блокировки. Более тога, по крайней мере, в Pthreads переменные условия координируются с мутексами для облегчения написания программ.

Использование передачи сообщений в приложениях может быть проще, чем использование потоков разделяемых переменных, но даже и в этом случае существуют опасности. Реализация шаблона producer/consumer фактически имеет четкий дефект. В частности не налагаются ограничения на размер очереди сообщений. В некоторый момент времени поток producer вызывает send, будет выделена памяти для запоминания сообщения, память не будет возвращена, пока сообщение не употребится. Если поток producer генерирует сообщения быстрее, чем consumer потребляет, то программа, в конце концов, исчерпает допустимую память. Это может быть зафиксировано ограничением размера буфера, но какой размер является приемлемым?

Выбор маленького буфера может вызвать взаимоблокировку, большого буфера – неэкономно. Эта проблема не имеет тривиального решения.

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

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

2.6. Интегрированная среда разработки прикладного программного

обеспечения

2.6.1. Средства разработки программ для встроенных систем на Си.

Существует как платные, так и бесплатные средства разработки программ для встроенных систем на Си. Мощное средство разработки бесплатно предоставляет компания Microsoft на своём интернет сайте [30]. Однако это средство довольно сложное и требует установки на компьютер с операционной системой Windows громоздких средств разработки Visual Studio (несколько гигабайт) и MSDN объё мом более 3 Гб, а также Windows Mobile SDK (около двух сотен мегабайт) и эмуляторов.

Средство под название Pelles C for Windows объемом около 8 Мб свободно доступно на сайте его разработчиков [31]. Данное средство разработки позволяет создавать разнообразные программы как под Windows CE (Windows Mobile), так для обычных персональных компьютеров под Windows. Данный пакет разработки включает в себя интерфейс среды разработки IDE, компилятор языка программирования Си, заголовочные файлы и библиотеки под разные платформы, набор полезных утилит, примеры кода и встроенный справочник среды разработки и стандарта языка программирования ISO C99 [32].

Проекты. В Pelles C проект включает в себя исходные файлы и команды для построения ординарного файла. Существует различные типы проектов для исполнимой программы (EXE), динамические библиотеки (DLL), статические библиотеки (LIB), так же как и разные ОС Windows CE и Windows. Только один проект может быть активным в каждый момент времени, но несколько проектов могут быть загружены в рабочую область (workspace). Когда проект загружен в IDE, он показывается в окне проекта (Project window). Окно проекта может показывать как исходные файлы (режим source view), так и выходные файлы (режим arget view), которые создаются во время сборки проекта.

Проект сохраняется в файле проекта (.ppj), дополнительные установочные параметры в файле расширения проекта (.ppx), а рабочая область в файле рабочей области (.ppw). Все они являются текстовыми файлами. Файл проекта в действительности является MAKEFILE со специальными макросами для IDE.

Редактор исходных текстов используется для редактирования некоторых текстовых файлов, например исходного Си-файла.

Редактор ресурсов используется для того чтобы визуально редактировать скрипты ресурсов (.rc). Как и другие редакторы IDE он имеет собственное меню.

Редактор изображений используется для визуального редактирования курсоров, пиктограмм и растровых отображений графических объектов (ресурсы CURSOR, ICON и BITMAP).

Отладчик используется для отладки программ (ещё бы!). Программа может содержать отладочную информацию в формате CodeView или COFF.

Программа POASM - Pelles Macro Assembler (Pelles макро-ассемблер) создает объектный файл (OBJ) в формате COFF (Common Object File Format) из исходного ассемблерного файла (ASM).

Программа POLINK – Pelles редактор связей создает исполняемые программы (EXE) или динамические библиотеки (DLL) из файлов библиотек и объектных файлов формата COFF.

2.6.2. Комплект программ Telelogic Tau SDL Suite

Telelogic Tau SDL Suite [33] является инструментом разработки и реализации программного обеспечения реального времени на SDL. SDL Suite состоит из графического редактора и синтаксического анализатора, симулятора и валидатора и нескольких оптимизирующих генераторов кода для компиляции исполнительного кода. На рис. 84 приведена структура SDL Suite.

Рис. 84. Структура SDL Suite

Органайзер (Organizer) является инструментом, который помогает разработчику при работе с SDL и MSC диаграммами. Органайзер может манипулировать текстовыми файлами, объектными моделями и Си-файлами (рис.85). Также органайзер координирует работу других инструментов SDL Suite.

Редактор SDL (SDL Editor) позволяет создавать, просматривать и редактировать SDL диаграммы. Редактор имеет различные режимы, зависящие от вида диаграмм. На рис. 86 приведено окно редактора в режиме блок-диаграммы, а на рис. 87 в режиме диаграммы процесса.

SDL анализатор (SDL Analyzer) проверяет SDL диаграмму на соответствие правилам синтаксиса и семантики, зафиксированных в рекомендации ITU-T Z.100.

Редактор MSC диаграмм (MSC Editor) позволяет создавать, просматривать и редактировать MSC диаграммы в соответствии с рекомендацией ITU-T Z.120. Можно разработать для проекта сценарии/случаи использования в виде MSC и наблюдать также в виде MSC результаты моделирования/валидации проекта (рис.88).

Рис. 85. Окно органайзера

Рис. 86. Окно редактора в режиме блок-диаграммы.

Рис. 87. Окно редактора в режиме диаграммы процесса.

Симулятор (Simulator) используется для тестирования и изучения динамики поведения спецификации системы (рис. 89). Симулятор работает как отладчик на уровне SDL. Во время моделирования можно наблюдать MSC диаграмму, SDL и текстовую трассировку.

Рис. 88. Окно редактора MSC диаграмм

Рис. 89. Окно симулятора

Обозреватель покрытия (Coverage Viewer) во время работы симулятора показывает какие части спецификации протестированы, а какие нет (рис. 90).

Валидатор (Validator) предоставляет механизм автоматизированного обнаружение неисправностей для проверки робастности приложения (устойчивости – мера способности системы восстанавливаться после ошибок или сбоев) и нахождение на ранней стадии проектирования несоответствия требованиям к ситеме. Это обычно относят к верификации системы на SDL. Когда сравнивают систему с требованиями к ней, Validator обеспечивает возможность выполнить автоматическую валидацию требований, выраженных в виде MSC диаграммы.

Рис. 90. Окно симулятора Coverage Viewer

2.6.3. Средства разработки программного обеспечения

встроенных систем SCADE

Семейство средств разработки SCADE от Esterel Technologies [34] предназначены для получения законченных решений разработчиками критических встроенных систем и их прикладного программного обеспечения.

Комплект программ SCADE Suite – это основанная на модели цепочка инструментов (tool-chain) для разработки прикладного программного обеспечения систем управления, интеграционную роль, в которой играет собственный (нативный, native) язык Scade и его формальная нотация. На рис. 91 приведена структура SCADE Suite. Это компоненты для создания проектов, моделирования и верификация проектов, генерации кода на Си и Ada и средства поддержки функциональной совместимости с инструментами разработки других производителей.

Унифицированная Методология Разработки Моделей в системе SCADE позволяет объединять алгоритмические описания, сделанные с помощью потоков данных, с описаниями, сделанными с помощью конечных автоматов, на любом уровне иерархии проекта. SCADE обеспечивает проектировщика технологией однократного безитерационного ввода информации, которая позволяет выполнить реализацию требований без избыточности или неоднозначности и построить более точные программные модели. В библиотеке SCADE содержится более трехсот дискретных операторов.

Эффективное Системное Проектирование. Шлюз к системам управления требованиями SCADE Requirements Management (RM) Gateway позволяет создавать связи прослеживаемости (traceability links) между системными требованиями, моделями, созданными в SCADE Suite и в SCADE Display, структурным дизайном, тестовым планом и проектной документацией.

Рис. 91. Структура SCADE Suite®

Система производства сертифицированного ПО SCADE предоставляет возможность ввода и обработки проекта системного уровня – спецификации требований, описания архитектуры на языке SysML/UML.

Шлюз SCADE SysML Gateway импортирует архитектуру, разработанную системными экспертами. Шлюз может работать с системами Telelogic Rhapsody и Artisan Studio™, а также легко адаптирован к другим средствам проектирования на языке SysML/UML.

Импорт из систем Simulink ™ и Stateflow выполняется в строгом соответствии с требованиями обеспечения безопасности, которые накладываются Унифицированной Методологией Разработки Моделей SCADE.

Верификация и Валидация на стадии проектирования. Симулятор SCADE Simulator исполняет встраиваемый код.

Верификатор проекта SCADE Suite Design Verifier предоставляет проектировщику возможность всестороннего исследования для поиска «краевых» ошибок, практически не детектируемых традиционными методами тестирования, и исправления их на самой ранней стадии проекта.

Тестовое Покрытие Моделей SCADE Model Test Coverage (MTC) оценивает полноту тестовой процедуры, разработанной на основе требований, и помогает достичь 100%-ого покрытия по MC/DC. MTC является средством верификации, квалифицированным по DO-178B

Масштабируемость до многопользовательских, территориально-распределенных проектов. Модульность SCADE-моделей обеспечивает безопасное и управляемое разделение труда между несколькими разработчиками или коллективами разработчиков.

Библиотеки позволяют совместное использование данных и функциональных блоков несколькими проектами, SCADE Suite обеспечивает согласованность в итоговых моделях.

SCADE Suite тесно интегрирован с системами управления требованиями, производимыми другими фирмами.

Генератор отчетов SCADE Reporter автоматически создает проектную документацию, обеспечивая ее постоянное обновление. Генерация отчетов может быть адаптирована к специальным требованиям путем настройки, управляемой из языка TCL. SCADE Reporter является средством разработки, квалифицированным по DO-178B.

Генерация эффективного, компактного и мобильного кода промышленного качества. Кодогенератор SCADE Code Generator производит код языка C стандарта ANSI, легко читаемый и прослеживаемый. Код независим от целевого процессора, не требует никаких специальных исполняемых библиотек или библиотек, специфичных для конкретного процессора. Код может исполняться на любом целевом микропроцессоре под управлением ОСРВ или без нее. В SCADE Suite кодом, можно задать автоматическое оформление для исполнения в среде операционных систем Integrity-178B™ (Green Hills Software), μC/OS-II (Micrium), PikeOS™ (Sysgo), VxWorks™ 653 (Wind River).

Кодогенерация, квалифицированная по DO-178B. Кодогенератор SCADE Suite Code Generator (KCG) является средством разработки, квалифицированным по DO-178B до Уровня A. Квалификационный комплект кодогенератора Qualification Kit предоставляет все артефакты (материалы),

требуемые для средств разработки (DO-178B 8110.49).

Эта квалификация позволяет разработчику исключить низкоуровневое тестирование сгенерированного кода и, поэтому, выполнять обновления дизайна быстро и без потери безопасности кода. Сгенерированный с помощью SCADE код используется более чем в 30-ти программах по сертификации и уже квалифицирован более чем в 20-ти программах.

Всесторонняя Сертификация Объектного Кода. Комплект верификации компилятора SCADE Compiler Verification Kit (CVK) позволяет провести верификацию применяемого компилятора языка C на корректность компиляции кода, сгенерированного в SCADE KCG. Комплект верификации подтверждает корректность работы сгенерированного кода по утвержденной методике, описанной в руководстве CAST 12.

Средство SCADE LifeCycle расширяет функциональность SCADE в направлении администрирования жизненного цикла критических приложений. Он интегрируется со всеми продуктами SCADE для обеспечения эффективности, полноты и долговременного обслуживания приложений SCADE. Особенностями комплекта является наличие в его составе компонент «Управления требованиями» (Requirements Management), автоматической «Генерации документов» (Documentation Generation), «Планов сертификации» (Certification Plans для сертификационного процесса DO-178B).

Средство SCADE System это инструмент разработки открытой архитектуры критической системы. Средство SCADE System базируется на стандартах SysML (Systems Modeling Language) и Eclipse. Используя SCADE System вместе с SCADE Suite, SCADE Display и SCADE LifeCycle, системные инженеры и программисты могут работать в одной инфраструктуре (framework), чтобы исключить дублирования усилий и несоответствия между описанием структуры системы и поведенческого описания ПО.

Модуль SCADE System Designer – инструмент моделирования проектов систем на архитектурном уровне позволяет системным инженерам моделировать проекты системных компонент и структуры с использованием блок-диаграмм SysML. Модуль также позволяет экспортировать структурные компоненты из какой-нибудь модели направлять их группам разработчиков подсистем.

Средство SCADE Display это гибкая графическая среда проектирования и развития для дисплеев и HMI (Human-Machine Interface, интерфейс "человек - машина") критических систем. Вместе с собственной поддержкой OpenGL (Open Graphics Library, графическое API) SC (Safety Critical, критическая безопасность) и стандартом ES (Embedded System), SCADE Display является новым поколением инструментов для разработки графики, макетирования остова, проектирования отображения, моделирования, верификации и валидации и квалифицированной генерации кода (KCG).

2.7. Валидация и оценка проекта

2.7.1. Моделирование, эмуляция и макетирование

Моделирование наиболее общая техника оценки и валидации проектов. Моделирование заключается в выполнении модели проекта на подходящем компьютерном оборудовании, обычно на компьютерах общего назначения. Очевидно, что модель должна быть выполнима. Все рассмотренные выполнимые модели и языки могут быть использованы в моделировании и на различных уровнях (системном, алгоритмическом, регистровых передач, вентильном). Уровень, на котором проекты моделируются, всегда является компромиссным между скоростью и точностью моделирования. Быстрее моделирование, меньше точность.

До сих пор использовался термин поведение в смысле функционального поведения системы (вход/выходное поведение). Существуют симуляторы не функционального поведения проектов, такие как симулятор теплового поведения, симулятор электромагнитной совместимости (EMC) с другим электронным оборудованием. Благодаря интеграции с физикой существует большое количество физических эффектов, которые могут быть включены в модель.

В кибер-физических системах моделирование сталкивается с серьезными ограничениями:

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

• Моделирование в физической среде может быть даже опасным.

• Для многих приложений может быть огромное количество данных и может быть невозможным промоделировать достаточное количество данных за приемлемое время.

• Большинство реальных систем также являются сложными. Следовательно, моделирование не может гарантировать отсутствие ошибок из-за того что не может быть выполнено полностью для всех возможных комбинаций входов и внутренних состояний.

Из-за этих ограничений усиливается акцент на валидацию с помощью формальной верификации. Тем не менее, сложные техники моделирования продолжают играть ключевую роль в валидации.

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

Для дальнейшего усиления правдоподобия можно продолжить замену моделируемых компонент реальными компонентами. Это не будут окончательные компоненты. Они могут быть приближением к реальным компонентам, но повышать точность моделирования.

Наиболее общим сейчас является представление об эмуляции одним компьютером другого в смысле программного обеспечения. Однако рассмотренное выше представление можно рассматривать как соответствующее общему, т.к. эмулируемый компьютер не просто моделируется, а предполагается, что его скорость выше, чем симуляция.

Быстрое макетирование (prototype)это такой процесс выполнения модели, когда ни один из компонент не представляется моделированием на хост компьютере. Все компоненты представлены реалистичными компонентами. Некоторые из них еще не окончательные компоненты (хотя это может быть реальная система). Существует много случаев, когда проекты должны быть испытаны в реалистичном окружении перед выпуском окончательной версией для производства.

Системы управления автомобилем хороший тому пример. Эти системы могут быть использованы водителями в различном окружении перед запуском в массовое производство. Так в автомобильной промышленности макетируют проекты. Эти макеты по существу ведут себя как окончательные системы, но они могут быть больше в размерах, с большим энергопотреблением и иметь другие свойства, которые мог привнести водитель-испытатель. Термин «макет» может ассоциироваться со всей системой, состоящей из электрических и механических компонент. Однако разница между быстрым макетированием и эмуляцией размыта. Быстрое макетирование само по себе широкая область деятельности, охватывающая не только встроенные системы.

Прототипы и эмуляторы могут быть построены, например, из FPGA. Шасси, содержащее FPGA, может быть размещено в корпусе пока водитель-испытатель упражняется с автомобилем. Этот подход не ограничивается автомобилестроением. Существуют несколько других случаев, когда макеты выполняются на FPGA. Коммерчески доступные эмуляторы состоят из большого числа FPGA. Они поставляются с необходимым инструментом для отображения проектируемой спецификации на эмуляторы. Используя этим эмуляторы, производят эксперименты с системами, которые ведут себя «почти» как окончательные системы. Однако каверзные ошибки при макетировании и эмуляции являются проблемой для сосредоточенных систем. Для распределенных систем ситуация еще более трудная.

2.7.2. Формальная верификация

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

Техники формальной верификации могут быть классифицированы по типу используемой логики.

Логика высказываний (пропозициональная логика). В этом случае модели состоят из булевых функций, а соответствующие инструменты называют Булевой проверкой, проверкой на тавтологию или проверкой на эквивалентность. Они могут быть использованы для проверки того что два представления булевых функций (или множества булевых функций) эквивалентны. На сегодня логика высказываний разрешима, она также разрешима независимо от того эквивалентны или нет два представления (нет сомнительных случаев). Например, одно представление может соответствовать вентилям реальной схемы, а другое спецификации. Доказательство затем эквивалентности доказывает, что результат всех преобразований (например, оптимизация энергопотребления или задержки) проекта являются корректными. Булева проверка может справиться с очень большими проектами с такими, как и исчерпывающая валидациия, основанная на моделировании. Ключевая причина мощи Булевой проверки заключается в использовании бинарного дерева решений (BDD). Сложность задачи проверки на эквивалентность булевых функций представленных BDD является линейной от числа узлов BDD. Напротив сложность задачи проверки на эквивалентность булевых функций представленных суммой произведений является NP-полной. Основанная на BDD проверка на эквивалентность по этой причине заменила симуляторы и работает со схемами из миллионов транзисторов.

Логика первого порядка (FOL). FOL включает операторы ∃ и ∀. Обычно допускаются также целые числа. Некоторая автоматизация для проверки FOL выполнима. Однако на сегодня FOL неразрешима. Это означает, что могут быть неопределенные случаи. Популярной техникой является исчисление Хоара (Hoare).

Логика высшего порядка (HOL). HOL базируется на лямбда-исчислении и позволяет манипулировать функциями так же как другими объектами. Для HOL доказательства едва ли когда-нибудь удастся автоматизировать и обычно должно выполняться вручную с некоторой поддержкой доказательства.

Логика высказываний может быть использована для проверки комбинационных логических схем. Она не может напрямую моделировать конечные автоматы. Для конечных автоматов необходимо оборвать обратные связи в схеме FSM и работать с несколькими копиями FSM, каждая из которых представляет результат воздействия одного входного набора (итерационная модель автомата с памятью). Однако этот метод не работает для длинных входных последовательностей.

С такими последовательностями может справиться техника «проверка модели» (model checking). Обычно проверка модели применялась для проектирования аппаратуры, но в последние 10-15 лет используется при разработке ПО. Эта техника использует темпоральную логику для задания спецификации, т.к. последняя способна выражать требования по безопасности для одновременных систем. Темпоральная логика является разновидностью модальной логики. Она изначально разрабатывалась для выражения таких модальностей как необходимость и возможность.

Темпоральная логика используется для рассуждения о знании, позволении, обязательстве.… Для текущего состояния она рассуждает о том, что есть истина на основании истинности или лжи атомарных высказываний. Она рассматривает выполнение системы как последовательность состояний, когда «текущее время» является индексом в последовательности. Будущее – более поздний индекс, прошлое – более ранний индекс.

Синтаксис темпоральной логики состоит из:

• p: примитивные высказывания;

• стандартные булевы связки (, ∨, ∧, ⇒);

• темпоральные операторы:

• Gφ φ всегда истинно (т.е. теперь и в будущем), глобально;

• Fφ φ истинно когда-нибудь в будущем;

• Xφ φ истинно в следующий момент времени;

• φUψ φ истинно пока не ψ истинно;

Задача проверки модели:

Пусть M граф переходов.

Пусть φ спецификация в темпоральной логике (темпоральная формула).

Найти все состояния s графа переходов M такие, что M, s⊨ φ.

В качестве примера рассмотрим микроволновую печь [35]. На рис. 92 приведена модель вычислений микроволновой печи в виде графа переходов M. Модель содержит четыре атомарных высказывания:

• Start: нажата кнопка – “start”;

• Close: дверца закрыта?;

• Heat: печь активна;

• Error: состояние ошибки.

Рис. 92. Граф переходов микроволновой печи

Состояния графа представляют ситуации (различные комбинации из атомарных высказываний), в которых может находиться система в различные моменты времени. Ребра могут иметь метки изображающие действия системы.

Рассмотрим свойство безопасности (спецификация), которое на естественном языке формулируется следующим образом: печь не нагревается, пока не закрыта дверь. Это свойство в виде темпоральной формулы имеет вид: (Heat) U Close. На рис. 93 приведено решение задачи проверки модели для микроволновой печи на соответствие свойству безопасности. Во всех состояниях свойство подтверждается.

Рис. 93. Проверка свойство безопасности микроволновой печи

Инструмент верификации, использующий техникупроверки модели, имеет два входа:

• модель, которую необходимо проверить;

• свойства, которые требуется проверить.

Инструмент верификации может доказать или опровергнуть свойства. В последнем случае он может предоставить контр пример (последовательность действий системы, на которой нарушается спецификация). Проверка модели легче автоматизируется, чем FOL.

EMC-система [36] интегрирует проверку модели и логику высшего порядка (рис. 94).

Рис. 94. EMC-система

Эта система принимает свойства, описанные как CTL формулы (Computation tree logic – логика вычислительного дерева). CTL формулы состоят из двух частей:

– квалификатор пути специфицирует пути в графе переходов;

– квалификатор состояния специфицирует состояния.

Например, M, s |= AGg означает, что в графе переходов M свойство g сохраняется для всех путей (обозначены как A), начинающихся в s и всех состояний (обозначены как G).