Литература
1.обратно | D. Dibois, H. Prade. Théorie des possibilités. Applications à la representation des connaissances en informatique. MASSON, Paris, Milan, Barselone, Mexico, 1988 (Дюбуа Д., Прад А. Теория возможностей. Приложения к представлению знаний в информатике: Пер. с фр. - М.: Радио и связь, 1990.) |
2.обратно | Ю. П. Пытьев. Возможность. Элементы теории и применения. М.: Эдиториал УРСС, 2000. |
3.обратно | сайт, посвященный технологии тестирования UniTESK и реализующим ее инструментам. |
4.обратно | А. В. Баранцев, И. Б. Бурдонов, А. В. Демаков, С. В. Зеленов, А. С. Косачев, В. В. Кулямин, В. А. Омельченко, Н. В. Пакулин, А. К. Петренко, А. В. Хорошилов. Подход UniTesK к разработке тестов: достижения и перспективы. (Опубликовано .) |
5.обратно | В. В. Кулямин, А. К. Петренко, А. С. Косачев, И. Б. Бурдонов. Подход UniTESK к разработке тестов. Программирование, 29(6): 25-43, 2003. |
6.обратно | А. Петренко, Е. Бритвина, С. Грошев, А. Монахов, О. Петренко. Тестирование на основе моделей. Открытые системы, №09/2003. (Опубликовано .) |
7.обратно | M. Fitting. Kleene's three-valued logics and their children. Fundamenta Informaticae, 20, 113-131, 1994. |
8.обратно | сайт Центра верификации операционной системы Linux. |
9.обратно | страница инструмента разработки тестов CTesK. |
10.обратно | сайт Института системного программирования РАН. |
11.обратно | I. Bourdonov, A. Kossatchev, A. Petrenko, and D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. FM'99: Formal Methods. LNCS 1708, Springer-Verlag, 1999, pp. 608-621. |
12.обратно | The RAISE Language Group. The RAISE Specification Language. Prentice-Hall BCS Practitioner Series. Prentice-Hall, Inc., 1993. |
13.обратно | А. В. Хорошилов. Спецификация и тестирование систем с асинхронным интерфейсом. Институт системного программирования РАН, Препринт 12, 2006. |
14.обратно | A. Tarski. Introduction to Logic and to the Methodology of Deductive Sciences. New York, 1941. (А. Тарский. Введение в логику и методологию дедуктивных наук. М.: ГИИЛ, 1948.) |
15.обратно | Я. А. Слинин. Современная модальная логика. Развитие теории алетических модальностей (1920 - 1960 гг.). Издательство Ленинградского университета, 1976. |
16.обратно | И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. Программирование. т. 29, № 5, стр. 245-258, 2003. |
1(обратно) | В дальнейшем эпитет неполный используется в отношении как, собственно, неполной, так и нечеткой информации, как и его синонимы неопределенный и не полностью определенный. |
2(обратно) | Часто вместо термина тестирование на основе моделей используется близкий термин тестирование на основе (формальных) спецификаций (specification based testing, specification-driven testing). |
3(обратно) | Исключение составляет обходчик ndfsm [], позволяющий обходить графы состояний для некоторого класса недетерминированных конечных автоматов. |
4(обратно) | В дальнейшем для краткости будем опускать эпитет функциональные и употреблять термин требования, понимая под ним именно функциональные требования. |
5(обратно) | Предполается, что варианты использования целевой системы известны, например, описаны в требованиях к системе. |
6(обратно) | На модальные функции возможности и необходимости обычно налагают некоторые ограничения, например, ◊P ≡ ¬ ? ¬ P и ?P ≡ ¬ ◊ ¬ P. |
7(обратно) | Обычно модальная логика интерпретируется с помощью системы возможных миров (possible worlds): в каждом возможном мире интерпретация задается двухзначной функцией истинности, а модальные функции определяются совокупностью значений истинности в возможных мирах. |
8(обратно) | Возможны и другие варианты определения семантики связок, например, так называемая короткая логика. |
9(обратно) | Факторизация задается отношением эквивалентности θ = { (x, y) Mc × Mc | f(x) = f(y) }. |
10(обратно) | Здесь для удобства маршрут представлен в виде последовательности вершин. |
11(обратно) | В этом случае объем требуемой памяти равен как минимум O(m(log n + X) + nI) вместо O(n(log n + I + X)), где n - число вершин, m - число дуг, I - размер идентификатора вершины, X - размер идентификатора стимула. |