Полнота. Библиографический список
 Скачать 1.42 Mb.
|
4. Рост интенсивности трафика IP-сети уменьшает длину интервала восстановления синхросигнала, что говорит о целесообразности использования выделенных служебных каналов с гарантированным качеством обслуживания (например, на базе технологии MPLS) под трафик синхронизации. Библиографический список 1. Timing and synchronization aspects in packet networks: Recommendation ITU-T G.8261. – 2008. 2. Circuit emulation service definitions, framework and requirements in Metro Ethernet Networks. Technical Specification MEF 3, 2004. 3. Решение проблем синхронизации в IP-сети / А. К. Канаев, А. С. Ванчиков, В. В. Кренев // Автоматика, связь, информатика. – 2011. – № 3. – С. 22–24. 4. Робастные методы обработки сигналов в радиотехнических системах синхронизации / А. В. Макшанов, А. В. Смирнов, А. К. Шашкин. – СПб. : С.- Петербургский гос. ун-т, 1991. –174 с. 5. Статистический анализ: подход с использованием ЭВМ / А. Афифи, С. Эйзен; пер. с англ. – М. : Мир, 1982. – 488 с. : ил. УДК 004.65: 004.052.42 М. Л. Глухарев МЕТОД ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ОГРАНИЧЕНИЙ ЦЕЛОСТНОСТИ И ТРИГГЕРОВ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ Верификация ограничений целостности и триггеров баз данных является актуальным направлением научных исследований и практических разработок. В настоящей статье рассматривается метод формальной верификации, основанный на метамодели требований целостности и позволяющий проверять функциональную корректность ограничений целостности и триггеров. функциональная корректность, формальная верификация, спецификация, реализация, требование целостности, ограничение целостности, триггер, триггерная связка, формальный описатель, метамодель формальных описателей, восстановление описателей, сравнение описателей. Введение Ограничения целостности (ОЦ) и триггеры являются программными объектами [1], предназначенными для поддержки целостности данных в таблицах баз данных (БД). Под функциональной корректностью ОЦ и триггеров понимается соответствие реализуемых ими функциональных возможностей требованиям заказчика, предъявленным до начала разработки БД. В настоящее время на практике функциональная корректность ОЦ и триггеров проверяется с помощью методов Вид ОЦ Типовой описатель PRIMARY KEY ( ) 1 ( ) если столбец; ( ( )) , COUNT x x is null x x t 1 2 1 2 (*) 1 ( ) ( ) ... ( ) , , ..., ( ( )) k k COUNT x is null x is null x is null x x x t , если x – группа столбцов x 1 , x 2 , …, x k UNIQUE ( ) 1 если столбец; ( ( )) , COUNT x x x t 1 2 (*) 1 , , ..., ( ( )) k COUNT x x x t , если x – группа столбцов x 1 , x 2 , …, x k NOT NULL если столбец; ( ) , x is null x t 1 2 ( ) ( ) ... ( ) ( ) k x is null x is null x is null t , если x – группа столбцов x 1 , x 2 , …, x k CHECK ( ) ( ) F x t FOREIGN KEY ' ( ') 1 ' ( ( )) \ ( ') ( ( ')) x x is not null x COUNT x x t t t , если x – столбец; ' ' 1 1 1 ' ' 1 , ..., , ..., (*) 1 , ..., ( ( )) \ ( ') ( ( ')) , k k k k x x x is not null x is not null x x COUNT x x t t t если x – группа столбцов x 1 , x 2 , …, x k Восстановление описателей по ОЦ сводится к следующей последовательности действий. 1. Информация обо всех ОЦ извлекается из системного каталога (системных таблиц) БД или файлов SQL-скриптов. 2. Тип каждого ОЦ определяется по ключевым словам PRIMARY KEY, FOREIGN KEY, UNIQUE, NOT NULL, CHECK. 3. По разновидности ОЦ определяется соответствующий типовой описатель, который и принимается в качестве описателя, восстановленного по ОЦ. В результате каждому ОЦ БД ставится в соответствие один и только один восстановленный описатель. 3.2 Восстановление описателей по кодам триггеров В описателе ( ) ( , ) | Tr Tr Tr Tr Desc Tr Q T C A множество T Tr включает таблицы и (или) псевдотаблицы, обрабатываемые триггером Tr, C Tr и является множеством столбцов таблиц из множества T Tr , а условие Q Tr – постусловием триггера Tr по Хоару [9], т. е. условием, которому должны удовлетворять все элементы множеств T Tr и C Tr на момент завершения работы триггера. A Tr является множеством DML-операций, активизирующих триггер. Восстановление описателя Desc(Tr) выполняется в следующем порядке. 1. В теле триггера выделяются возможные маршруты выполнения M 1 , …, M L 2. Выполняется семантический анализ всех маршрутов (M 1 , …, M L ), цель которого – синтез постусловий этих маршрутов ( L M M Q Q ..., , 1 соответственно). Этот процесс циклический, на каждом шаге цикла выполняется синтез постусловия одного (текущего) маршрута. 2.1. Текущий маршрут M представляется в виде последовательности C 1 , A 1 ; …; C N , A N , где A 1 , …, A N – простые SQL-операторы, а C 1 , …, C N – условия передачи управления операторам A 1 , …, A N соответственно. Под простыми операторами в данном случае понимаются DML-операторы, непосредственно влияющие на состояние данных в БД (INSERT, UPDATE, DELETE, ROLLBACK TRAN), а также пустой оператор. Оператор SELECT не изменяет состояния данных, но SQL-конструкции на его основе могут использоваться в условиях C 1 , …, C N . Если передача управления оператору A i производится безусловно, то C i принимается тождественно равным единице. Если A i – пустой оператор, это означает передачу управления оператору A i+1 по условию 1 i i C C 2.2. Каждому оператору A i текущего маршрута ставится в соответствие собственное постусловие Q i – постусловие, определяемое непосредственно на основе семантики оператора A i при рассмотрении данного оператора изолированно от прочих операторов маршрута. 2.3. Выполняется собственно синтез постусловия Q M текущего марш- рута M с использованием алгоритма, блок-схема которого представлена на рисунке. Алгоритм использует множество предикатов U, в которое последовательно включаются предусловие маршрута (блок 1), условия C i (блок 4) и собственные постусловия операторов Q i (блок 12). До включения Q i в множество U выполняется инверсия тех текущих элементов этого множества, ложность которых следует из условия Q i (блоки 8–11). В блоках 1, 4, 12 множество U определяется с помощью знака двоеточия. Тем самым подчеркивается, что данное множество содержит не результаты вычисления логических выражений u j (т. е. не значения 1 и 0), а сами логические выражения. Аналогичным образом и с аналогичной целью в блоках 6 и 14 обозначена операция определения постусловия Q M как конъюнкции или отрицания конъюнкции всех условий, входящих в множество U. Постусловие Q M формулируется по окончании прохождения маршрута, в тот момент, когда множество U является окончательно сформированным. Если маршрут завершается оператором ROLLBACK TRAN, то Q M определяется как отрицание конъюнкции всех элементов множества U; в остальных случаях – как конъюнкция элементов без отрицания. Алгоритм синтеза постусловия маршрута 3. В качестве постусловия триггера принимается дизъюнкция синтезированных постусловий маршрутов: 1 L Tr M M Q Q Q 4. Формируется множество DML-операций A Tr , которое соответствует множеству активизирующих операторов, указанных в теле триггера. Начало U : {P} i := 1 i ≤ N A i ROLLBACK TRAN j := 1 j ≤ |U| j := j + 1 i := i + 1 Конец да да да да нет нет нет нет 1 2 3 4 5 6 7 8 9 10 11 12 13 14 3.3 Восстановление описателей по триггерным связкам Результатом восстановления описателей является множество описателей реальных функций целостности БД. Если в этом множестве существует группа описателей с эквивалентными условиями Q, то существует соединение этих описателей, являющееся формальной моделью одной реальной функции целостности [9]. Типичным примером такой ситуации является использование триггерной связки в БД. Пусть имеются триггеры Tr 1 ; …; Tr q – такие, что ( ) ( , ) | ; 1, i i Desc Tr Q T C A i q , т. е. восстановленные по триггерам описатели одинаковы в части условия Q, но различаются множествами операций. Очевидно, что триггеры в совокупности реализуют одну функцию целостности, т. е. образуют связку размером q. Соединение описателей, восстановленных по триггерам, является описателем этой функции целостности: 1 1 ( ; ...; ) ( , ) | q q Desc Tr Tr Q T C A A . (2) Описатель 1 ( ; ...; ) q Desc Tr Tr допустимо считать описателем, восстановленным по триггерной связке. Восстановление описателей по триггерным связкам в БД, таким образом, удобно выполнять в следующем порядке. 1. Восстанавливают описатели по триггерам целевой БД. 2. В полученной модели реализации функций целостности выделяют группы описателей, имеющих эквивалентные условия Q. 3. Соединяют между собой описатели с эквивалентными условиями. Соединения описателей заменяют группы описателей по триггерам, на основе которых они получены. На этом процесс восстановления описателей завершается, и его результатом является перечень описателей, восстановленных по ОЦ, триггерам и триггерным связкам. 4 Сравнение описателей БД можно считать корректно реализованной в части ОЦ и триггеров, если каждому восстановленному описателю соответствует исходный описатель заранее декларированного требования целостности, и наоборот. Задача сравнения описателей состоит в том, чтобы для каждого описателя из спецификации найти эквивалентный ему восстановленный описатель в реализации, а для каждого описателя в реализации – эквивалентный ему описатель в спецификации. Описатели называются эквивалентными, если эквивалентны их условия Q и равны их множества A. Описатель, которому не соответствует эквивалентный описатель в противоположной модели, назовем несоответствующим описателем. Наличие несоответствующего описателя в спецификации свидетельствует о том, что представленному в нем требованию Validation Issues in Databases, Knowledge-Based Systems and Ontologies. – N. Y., John Wiley & Sons Inc., 2001, 16(3), pp. 285–306. 5. Программа для автоматизированной верификации ограничений целостности баз данных / М. Л. Глухарев, А. П. Косаренко, А. Д. Хомоненко // Программные продукты и системы. – 2011. – № 1 (93). – С. 91–95. 6. An axiomatic basis for computer programming / C. A. R. Hoare // Communications of the ACM, 12(10), pp. 576–585, October 1969. 7. Assigning meaning to programs / R. W. Floyd, J. T. Schwartz // Proc. of Symposium in Applied Mathematics, ed. Mathematical Aspects of Computer Science, 19:19-32, 1967. 8. Дисциплина программирования / Э. Дейкстра. – М. : Мир, 1978. – 275 с. 9. Применение формальных описателей для логико-алгебраического моделирования требований целостности информации в реляционных базах данных / М. Л. Глухарев // Известия Петербургского университета путей сообщения. – 2010. – Вып. 4 (25). – С. 78–88. УДК 624.15 А. В. Горбушин РАЗРАБОТКА МЕТОДИКИ ОПРЕДЕЛЕНИЯ НЕСУЩЕЙ СПОСОБНОСТИ СВАИ С УШИРЕНИЯМИ ПО ДАННЫМ СТАТИЧЕСКОГО ЗОНДИРОВАНИЯ Представлены результаты эксперимента с модельными сваями, имеющими одно и два уширения. Предлагается методика расчета буронабивных свай с одним и двумя уширениями на основе данных сопротивления грунта под конусом зонда по данным статического зондирования. буронабивные сваи с уширениями, статическое зондирование. Введение Серьезной проблемой при геотехническом строительстве в центральной части Санкт-Петербурга является значительная мощность слабых грунтов. Буроинъекционные и буронабивные сваи, изготовленные в таких грунтах, имеют, как правило, большую длину для обеспечения необходимой несущей способности (НС) сваи по грунту. Решение задачи обеспечения НС свай при уменьшении их длины возможно по следующим направлениям: 1. Увеличение площади опирания и боковой поверхности свай (устройство свай с уширениями, пирамидальных свай и т. д.). 2. Увеличение несущих свойств примыкающего к телу сваи грунта (сваи по технологии «Титан», РИТ; сваи, образованные в результате принудительного отжатия (вытеснения) грунта и буроинъекционные [1]). |
недекларированных возможностей (НДВ), особенно умышленных [5].
Динамическое тестирование ОЦ и триггеров целесообразно дополнять
формальной верификацией, которая основана на нахождении формального соответствия между спецификацией и реализацией проверяемого объекта; под спецификацией понимается модель требований к объекту, а под реализацией – модель реальных свойств (функциональных возможностей) объекта. Широко известны методы логико-аналитической верификации программ, предложенные Ч. Хоаром [6], Р. Флойдом [7], Э. Дейкстрой [8] и другими авторами. Однако эти методы не адаптированы к ОЦ и триггерам БД, и в целом вопросы формальной верификации ОЦ и триггеров не имеют достаточной теоретической проработки.
Исходя из вышесказанного, следует заключить, что разработка метода формальной верификации ОЦ и триггеров реляционных БД является актуальной задачей в области обеспечения качества
БД и автоматизированных информационных систем в целом.
1 Метамодель требований целостности как основа формальной
верификации ограничений целостности и триггеров
При использовании метода формальной верификации ОЦ и триггеров в качестве спецификации применяют набор формальных описателей
(далее – описателей) требований целостности, где каждый описатель является логико-алгебраической моделью одного и только одного требования [9].
В общем виде описатель представляется как выражение вида:
( , ) |
Q T C
A
, (1) где
T
– множество таблиц, связанных требованием целостности;
C – множество столбцов таблиц, входящих в множество T и связанных данным требованием;
( , )
Q T C
– условие требования, связывающее все элементы множеств T, C;
A – множество операций записи данных; если
1
{ , ..., }
n
T
t
t
, то
1
{
( ),
A
ins t
1 1
( ),
( )}
{
( ),
( ),
( )}
n
n
n
upd t
del t
ins t
upd t
del t
;
ins(t) – предикат выполнения вставки строк в таблицу t;
upd(t) – предикат выполнения обновления строк таблицы t;
del(t) – предикат выполнения удаления строк из таблицы t.
Выражение (1) имеет следующий смысл: условие
)
,
(
C
T
Q
должно быть истинно после выполнения любой операции из множества A.
Описатель является не только логико-алгебраической формулировкой требования целостности, но и спецификацией программных объектов,
декларативная реализация с помощью ОЦ;
процедурная реализация с помощью одиночного триггера;
процедурная реализация с помощью совокупности одновременно работающих триггеров, образующих триггерную связку.
Описатель требования целостности, таким образом, может быть спецификацией ОЦ, триггера или триггерной связки. Допустимо утверждать, что совокупность всех описателей требований целостности образует спецификацию БД в части всех ее ОЦ и триггеров.
С другой стороны, реальные функции целостности также допустимо и удобно моделировать с помощью описателей. Совокупность описателей реальных функций целостности БД можно называть реализацией БД в части ОЦ и триггеров.
Задача формальной верификации ОЦ и триггеров – подтвердить полное соответствие друг другу описателей требований и функций целостности или выявить несоответствия между ними.
2 Этапы верификации
Исходными данными для проведения формальной верификации ОЦ и триггеров являются:
формальные описатели требований целостности;
SQL-коды ОЦ и триггеров проверяемой БД.
Верификация проводится в два этапа.
Первый этап – восстановление описателей – представляет собой построение модели реализации ОЦ и триггеров. На этом этапе эксперт
(инженер по тестированию) проводит семантический анализ SQL-кодов
ОЦ и триггеров, стремясь понять, какие именно функции целостности они реализуют. Результатом этих действий является набор описателей реализованных функций целостности – восстановленных описателей.
Второй этап – сравнение описателей – определяет несоответствия между спецификацией и реализацией.
По результатам верификации принимается решение о допуске БД к эксплуатации или о доработке требований целостности, ОЦ и триггеров.
3 Восстановление описателей
3.1 Восстановление описателей по кодам ограничений целостности
Восстановление описателей по кодам ОЦ не представляет трудности.
Каждому типовому ОЦ, поддерживаемому реляционными СУБД, можно поставить в соответствие типовой описатель. Это соответствие показано в таблице, где символом
t
обозначено имя таблицы БД, к которой привязано
ОЦ, а x – связанный столбец или группа связанных столбцов.
ТАБЛИЦА. Соответствие между видами ОЦ и описателями типовых требований целостности, накладываемых на столбцы x таблицы t
Вид ОЦ
Типовой описатель
Наличие несоответствующего описателя в реализации свидетельствует о том, что представленной в нем реальной функции целостности в точности не соответствует ни одно из заявленных требований, т. е. в данном описателе представлена НДВ, влияющая на состояние данных в таблицах и (или) псевдотаблицах.
Таким образом, в процессе сравнения выявляются:
специфицированные и реализованные функции целостности;
специфицированные, но не реализованные функции;
реализованные, но не специфицированные функции, т. е. НДВ в ОЦ и триггерах.
Результат сравнения описателей включает количество корректно реализованных требований целостности, перечень и количество несоответствующих описателей-спецификаций, перечень и количество несоответствующих восстановленных описателей, долю нереализованных требований целостности от общего числа требований и долю несоответствующих описателей (НДВ) от общего числа реальных функций целостности.
Заключение
Рассмотренный метод формальной верификации ОЦ и триггеров реляционных БД позволяет проводить анализ БД на соответствие формальным требованиям целостности, находить случайные и умышленные дефекты в ОЦ и триггерах, не прибегая к составлению сложных тестовых сценариев. В случае, когда ОЦ и триггеры функционально некорректны относительно предъявленных требований, разработанный метод верификации позволяет получить логико- алгебраическое описания свойств НДВ, влияющих на состояние данных в
БД.
Библиографический список
1. Базы данных : учебник для высших учебных заведений / А. Д. Хомоненко,
В. М. Цыганков, М. Г. Мальцев; под ред. проф. А. Д. Хомоненко. – 3-е изд., доп. и перераб. – СПб. : Корона Принт, 2003. – 665 с. – ISBN 5-7931-0168-3.
2. A Tool for Generating Test Case from Relational Database Constraints Testing /
Tongrak P., Suwannasart T. // Computer Science and Information Technology (ICCSIT
2009). 2nd IEEE International Conference on Date: Aug. 8–11. Beijing, China, 2009, pp. 435–439.
3. A Framework for Checking Integrity Constraints in a Distributed Database /
A. A. Alwan, H. Ibrahim, N. I. Udzir // ICCIT 08. Third International Conference on
Convergence and Hybrid Information Technology. – Vol. 1. Busan, Korea, Nov. 11–13, 2008, pp. 644–650.
4. Optimizing Fragment Constraints – a Performance Evaluation / Ibrahim H.,
Gray W. A. and Fiddian N. J. // International Journal of Intelligent Systems – Verification and