http://se.ethz.ch/~meyer/publications/computer/test_themselves.pdf
В статье описывается система AutoTest, позволяющая повысить эффективность использования программных контрактов. Система позволяет:
1) автоматически генерировать test case'ы (в основном, случайным образом выбирая аргументы вызываемых методов)
2) следить за работой программы и генерировать test case'ы, на которых произошли precondition failure или postcondition failure
3) вручную задавать test case'ы.
Russian researcher blog
Заметки системного программиста
суббота, 25 декабря 2010 г.
воскресенье, 12 декабря 2010 г.
Задача построения идеального транслятора для VLIW-архитектуры
Для ускорения выполнения последовательная программа исполняется современными микропроцессорами почти всегда с использованием различных методов явного или неявного распараллеливания. Задача состоит в том, чтобы в явном виде подготовить исходную последовательную программу в таком виде, чтобы максимизировать ее распараллеливание на микропроцессоре. Естественно, задача имеет смысл только при задании класса архитектур и класса программ.
четверг, 2 декабря 2010 г.
Задача верификации спецификаций
Для верификации программ придумано множество различных методик. В том числе, например, "верификация на модели" (model checking), когда верифицируется не сам код программы, а его модель (обычно некая система переходов или автомат специального вида). На таких моделях успешно проверяется выполнение ряда свойств (например, отсутствие взаимоблокировок, дедлоков, в мультипроцессном коде).
Но почему бы не посмотреть на верификацию спецификаций? Ведь для спецификаций тоже можно формулировать свойства и проверять их! Задача состоит в определении таких свойств и предложению методов верификации спецификаций на выполнение этих свойств.
Сложность:
постановка задачи (непонятно, что это за свойства, о каких спецификациях идет речь)
вычислительная сложность (как и любая верификация)
Но почему бы не посмотреть на верификацию спецификаций? Ведь для спецификаций тоже можно формулировать свойства и проверять их! Задача состоит в определении таких свойств и предложению методов верификации спецификаций на выполнение этих свойств.
Сложность:
постановка задачи (непонятно, что это за свойства, о каких спецификациях идет речь)
вычислительная сложность (как и любая верификация)
Задача автоматического поиска обобщенного состояния
Речь идет о тестировании программ. Программы запускаются различными способами и проверяется, что во всех этих запусках программы ведут себя так, как положено. Вопрос только в том, что это за способы и как реализовать эти способы (задача проверки работы программы решена куда лучше).
Рассмотрим программу (или компонент программы), поведение которой описывается конечным автоматом. Тогда под "способами" можно понимать запуски, в которых достигаются заданные состояния автомата, переходы в автомате или даже целые пути. Но проблема в том, что размеры автомата огромные. Поэтому состояния автомата группируют согласно некому отношению эквивалентности и полученный автомат называют "обобщенным автоматом". Задача состоит в автоматическом построении таких обобщенных автоматов. Обобщенный автомат не должен стать недетерминированным, если исходный был детерминированным, ну и количество состояний в обобщенном автомате должно-таки позволять проводить тестирование в приемлемые человеческие сроки.
Сложность:
постановка задачи (четко надо понять, какие автоматы называются "обобщенными" и о каком отношении "обобщения" идет речь),
вычислительная сложность (перебор всех разбиений множества состояний автомата)
Рассмотрим программу (или компонент программы), поведение которой описывается конечным автоматом. Тогда под "способами" можно понимать запуски, в которых достигаются заданные состояния автомата, переходы в автомате или даже целые пути. Но проблема в том, что размеры автомата огромные. Поэтому состояния автомата группируют согласно некому отношению эквивалентности и полученный автомат называют "обобщенным автоматом". Задача состоит в автоматическом построении таких обобщенных автоматов. Обобщенный автомат не должен стать недетерминированным, если исходный был детерминированным, ну и количество состояний в обобщенном автомате должно-таки позволять проводить тестирование в приемлемые человеческие сроки.
Сложность:
постановка задачи (четко надо понять, какие автоматы называются "обобщенными" и о каком отношении "обобщения" идет речь),
вычислительная сложность (перебор всех разбиений множества состояний автомата)
Задача автоматического поиска дефекта в программе
Программы содержат ошибки, это факт. И от ошибок надо избавляться. Вот только весь вопрос в том, как и какими средствами. В данной задаче речь идет об автоматическом поиске входных данных данной программы (куда включается в том числе состояние среды, в которой работает программа), при запуске на которых программа "упадет". Можно рассматривать частный случай этой задачи: есть одна функция (с публичным доступом), требуется автоматически определить входные данные функции, на которых она "упадет".
Сложность:
вычислительная сложность (перебор всех входных данных)
Сложность:
вычислительная сложность (перебор всех входных данных)
Задача автоматического распараллеливания последовательных программ
Есть такая светлая идея, что последовательный алгоритм может быть эффективно распараллелен. Конечно, речь идет о специальных параллельных архитектурах и о специальном классе последовательных алгоритмов. Задача состоит в том, чтобы выделить такие классы программ и архитектур и предложить методы автоматического распараллеливания.
Сложность:
сложность постановки задачи,
вычислительная сложность
Сложность:
сложность постановки задачи,
вычислительная сложность
Проверка корректности самоизменяющихся программ
Задача состоит в том, чтобы по данной программе (возможно, лишь в бинарном виде) определить:
1) портит ли она "полезные" данные (т.е. есть данные, которые она портить не должна)
2) передает ли она несанкционированным образом третьей стороне какие-либо данные
Примеры самоизменяющихся программ: вирусы
Синонимы: "полиморфный" код (то же, что и самоизменяющийся)
Сложность:
сложность постановки задачи (неточно сформулировано то, что надо проверять),
вычислительная сложность (проанализировать все пути выполнения)
1) портит ли она "полезные" данные (т.е. есть данные, которые она портить не должна)
2) передает ли она несанкционированным образом третьей стороне какие-либо данные
Примеры самоизменяющихся программ: вирусы
Синонимы: "полиморфный" код (то же, что и самоизменяющийся)
Сложность:
сложность постановки задачи (неточно сформулировано то, что надо проверять),
вычислительная сложность (проанализировать все пути выполнения)
Подписаться на:
Сообщения (Atom)