Перечислите примитивы синхронизации по стандартам POSIX

Назовите некоторые группы API, определяемые стандартом POSIX.

Назовите известные вам программные инструменты формальной верификации ПО.

Верификация – проверка корректности результатов некоторого этапа разработки по отношению к требованиям, сформулированным на предыдущих этапах.

Формальная верификация состоит из: формальная проверка, результаты и требования должны быть представлены в виде формальных моделей (результат = реализация, требования = спецификация), соответствие м-ду ними должно быть определено формально.

Полное модлирование:

n Дедуктивный анализ
(theorem proving) Floyd – 1967

n Проверка моделей
(model checking) Clarke, Emerson – 1981

n Проверка симуляции
(simulation checking, equivalence checking) Moore – 1956

n Символическое выполнение
(symbolic execution) Topor, Burstall – 1972

n Абстрактная интерпретация
(abstract interpretation) Cousot – 1975

Неполное моделирование:

n Формальное тестирование
(formal conformance testing) Василевский – 1973
Hennessy, DeNicola – 1984

Верификационный мониторинг
(runtime verification, passive testing)
С 1970-х было много работ, в которых этот термин не употреблялся
~1999 – термин (Havelund, Rosu?)

146. Какой из подходов формальной верификации ПО может быть полностью автоматизирован?

Проверка моделей

147. Для ПО какого назначения и сфер применения следует использовать формальную верификацию?

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

148. В чём преимущество формальной верификации ПО по сравнению с тестированием?

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

149. Какой вид переносимости программ определяет стандарт POSIX?

на уровне исходных кодов

Интерфейс командной строки.

Большинство систем поддерживает терминальный (последовательный) интерфейс POSIX для изменения параметров, таких как скорость передачи, размер символов и т.д.

мьютэксы, условные переменные,

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

152. Сколько степеней соответствия ОС стандартам POSIX имеется? Чем они отличаются?

Стандарт POSIX.1 содержит несколько сотен (если не тысяч) требований; считается самоочевидным, что если не выполнено хотя бы одно из них, то система (или прикладная программа) не удовлетворяет стандарту. Вместе с тем, к настоящему времени написано такое количество операционных систем класса UNIX и прикладных программ для них, что вряд ли разумно требовать полного соответствия в указанном смысле. Трудности разработки международного стандарта такого рода усугубляются существованием разных национальных языков. Даже если забыть о прикладных программах, предназначенных для обработки текстов на национальных языках, практически любая прикладная программа должна выдавать какие-то диагностические сообщения и/или воспринимать тексты, вводимые оператором.

Осознавая такого рода трудности, авторы POSIX предлагают уточненную семантику слова "соответствует". Во-первых, вводится несколько видов соответствия (прикладной программы стандарту):

строгое соответствие стандарту POSIX.1;

соответствие международной версии POSIX.1;

соответствие национальной версии POSIX.1;

соответствие POSIX.1 с расширениями.

Дата добавления: 2014-12-24