Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Національна академія наук України

Інститут кібернетики імені В.М. Глушкова

Автореферат

дисертації на здобуття наукового ступеня кандидата фізико-математичних наук

01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем

Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів

Летичевський Олександр Олександрович

Київ - 2005

Дисертацією є рукопис.

Робота виконана в Інституті кібернетики ім. В.М. Глушкова НАН України.

Науковий керівник: доктор фізико-математичних наук, професор Капітонова Юлія Володимирівна, Інститут кібернетики ім. В.М. Глушкова НАН України, завідуюча відділом

Офіційні опоненти:

доктор фізико-математичних наук, професор Асельдеров Зайнутдін Макашаріпович, Національний технічний університет України ”КПІ”,

кандидат фізико-математичних наук Бублик Володимир Васильович, Київський національний університет імені Тараса Шевченка

Провідна установа: Інститут програмних систем НАН України, відділ теорії комп'ютерних обчислень

Учений секретар спеціалізованої вченої ради Синявський В.Ф.

Анотація

Летичевський О.О. Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем. - Інститут кібернетики ім. В.М. Глушкова НАН України. - Київ, 2005.

Дисертація присвячена побудові методів роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Розглянуто п'ять складових частин цієї технології: формалізація вимог у вигляді базових протоколів; пошук суперечливостей та неповноти; генерація тестових наборів з множини вимог; синтез та аналіз динамічних властивостей моделі. В розробці методів використовуються методи алгебраїчного та інерційного програмування, а також формалізм алгебри процесів, зокрема властивості атрибутних транзиційних систем. Вимоги до інтерактивних систем представляються у вигляді формальних специфікацій - базових протоколів. Визначено клас базових протоколів, для якого задачі технології вирішуються без експонентного вибуху. За допомогою розробленого у роботі формалізму будуються алгоритми верифікації базових протоколів з використанням машини доведення, а також синтез моделі за базовими протоколами. На основі створених методів символьного моделювання розглядаються різні критерії генерації тестів та їх застосування до генерації тестів за специфікаціями, записаними сучасними інженерними мовами, - MSC, SDL, UML.

Ключові слова: атрибутні транзиційні системи, агенти та середовища, алгебра процесів, вимоги до програмного забезпечення, базові протоколи, верифікація, символьне моделювання, суперечливість та неповнота специфікацій, автоматичне доведення теорем, генерація тестів.

Аннотация

Летичевский А.А. Верификация и тестирование интерактивных систем, специфицированных с помощью базовых протоколов. - Рукопись.

Диссертация на соискание научной степени кандидата физико-математических наук по специальности 01.05.03 - математическое и программное обеспечение вычислительных машин и систем. - Институт кибернетики им. В.М. Глушкова НАН Украины. - Киев, 2005.

Диссертация посвящена построению методов работы с требованиями, которые составляют технологию, являющуюся составной частью процесса создания программных систем с большим количеством состояний. Рассматривается пять составных частей технологии: формализация требований в виде базовых протоколов; поиск противоречивостей и неполноты; генерация тестовых наборов из множества требований; синтез и анализ динамических свойств модели. В разработке методов используются методы алгебраического и инсерционного программирования, в частности понятия агента, среды и функции погружения. Для описания семантики базовых протоколов используется формализм алгебры процессов и свойства атрибутных транзиционных систем. Для базовых протоколов, которые представляют требования в виде формальных спецификаций, определено класс, для которого задачи технологии решаются без экспоненциального взрыва - класс протоколов с одним ключевым агентом. С помощью разработанного в работе формализма строятся алгоритмы верификации базовых протоколов с использованием доказательной машины, а также синтез модели по базовым протоколам. Разделяются статические и динамические свойства, которые необходимо верифицировать. К статическим свойствам относятся непротиворечивость и неполнота системы базовых протоколов. Динамические свойства проверяются на синтезированной модели методом описания и доказательства аннотаций. К таким свойствам относятся безопасность и достижимость.

На основе созданных методов символьного моделирования рассматриваются различные критерии генерации тестов и их использование в генерации тестов по спецификациям, записанным с помощью современных инженерных языков - MSC, SDL, UML. В методах символьного моделирования используются понятия прямого и обратного предикатного трансформера, с помощью которого осуществляется генерация символьных трасс, которые в дальнейшем преобразуются в набор тестов.

Созданные автором прототипы программ, реализующих рассмотренные методы, являются основой системы верификации требований, разработанной и внедренной для работы с требованиями в промышленных телекоммуникационных моделях в кампании Motorola, а также в кампании “Информационные программные системы”.

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

Abstract

Letychevskyy O.O. Verification and Testing of Interactive Systems Specified by Basic Protocols.

Thesis for the degree of candidate of physical and mathematical sciences on the speciality 01.05.03 - mathematical and software support of computing machines and systems. - Glushkov Institue of Cybernatics of Ukrainian Academy of Sciences. -Kyiv, 2005.

The thesis is devoted to the methods for processing of requirements. These methods form the technology that is a part of process of software creation for the program systems with large amount of states. Five parts of technology is considered - formalization of requirements as basic protocols, searching of inconsistencies and incompleteness, test generation from the set of basic protocols, synthesis and analysis of dynamic properties of model. Methods of algebraic and insertion programming are used in development. Processes algebra is used in formalisms development especially properties of attributes transition systems. It is defined the special class of basic protocols, that presented the requirements as the set of formal specifications. This class is suitable for the resolving technology tasks without exponential explosion. Correspondingly to developed formalism the algorithms of verification are created in thesis with usage of proving machine. The synthesis of model correspondingly to the set of basic protocols is considered in thesis. The different criteria of test generation are considered by means of symbolic modeling methods. These criteria are used for test generation from specifications created as modern engineer languages - MSC, SDL, UML.

Key words: attribute transition systems, agents and environments, process algebra, software requirements, verification, symbolic modeling, inconsistency and incompleteness of specifications, automatic theorem proving, test generation.

1. Загальна характеристика роботи

телекомунікаційний верифікація інсерційний програмування

Актуальність теми. Верифікація і тестування систем є найважливішими задачами, вирішення яких визначає якість програмного забезпечення. Сучасні індустріальні програмні системи, що використовуються, зокрема в галузі телекомунікацій, нараховують десятки тисяч вимог. Тому при їх створенні імовірність появи помилок досить висока. Використання методів верифікації вимог для виявлення помилок уже на етапі збору вимог дозволить зменшити кількість помилок, які визначаються на етапі кодування, і відповідно скоротити час розробки систем та підвищити їх якість. З іншого боку, створення набору символьних тестів, що покриває усі вимоги, є найважливішою задачею тестування індустріальних систем.

У сучасній літературі існує клас методів, призначений для автоматичного аналізу формальних специфікацій і генерації з них тестів. Методи цього класу розбиваються на дві частини. Перша частина належить до так званого Model Checkіng - перевірки моделі, заданої формальними специфікаціями, а друга - пов'язана з доказом тверджень, що характеризують поводження системи, наприклад, її критичних властивостей - lіveness (життєздатність), safety (цілісність) і т.п. Model Checkіng, в основному, застосовується до формальної верифікації систем з скінченним числом станів. Формалізовані вимоги виражені формулами темпоральної логіки, а ефективні символьні алгоритми використовуються для обробки моделі і перевірки, чи відповідають вони вимогам, чи ні. Для перевірки систем з великою кількістю станів використовуються системи Verіsoft, SMV, SPІ, SCR, Murphі. Основною проблемою даного підходу є проблема експоненційного вибуху множини досліджуваних станів.

До систем, що працюють з доказами тверджень, належить система HOL, яка є середовищем для інтерактивного доказу теорем у логіці вищих порядків. Система PVS також працює з логіками вищих порядків і абстрактних типів даних.

Використання цих методів було успішно впроваджене стосовно специфікацій, виражених мовами MSC, SDL, UML, які всіляко застосовуються в інженерних розробках. Фірми Telelogіc і іLogіc брали участь у проекті OMEGA, що призначався з метою розробки формальних засобів для застосування на різних стадіях дизайну UML-специфікацій. У корпорації Sіemens була проведена верифікація частини GSM-протоколу з використанням засобів SVE. Інтегрована система для обробки SDL-специфікацій була реалізована на базі доказової машини ACL2.

Мова MSC також є одним з об'єктів застосування формальних методів. Система PTK реалізує автоматичний синтаксичний і семантичний аналіз MSC і генерує тестові специфікації різними мовами, такими як SDL, TTCN і С. FatCat, призначений для пошуку недетермінованих випадків у MSC-діаграмах.

Вищевказані системи, з одного боку, були в основному призначені для вирішення наукових задач, і входом у систему були формальні специфікації, записані деякою спеціальною мовою, складної для розуміння інженерами. Ця обставина визначила одну з основних перешкод на шляху широкого впровадження формальних методів у інженерну практику. Іншою проблемою, яку не вдалося, вирішити, виявилась проблема верифікації систем з нескінченним або дуже великим простором станів.

Таким чином, проблема використання формальних методів для верифікації вимог та генерації тестів в інженерній практиці із застосуванням мов MSC, SDL та UML є актуальною проблемою. Вказана задача вирішується у даній роботі для спеціального класу вимог, названих К-протоколами. Для вирішення поставлених задач використовуються методи алгебраїчного та інсерційного програмування у комбінації з методами автоматичного доведення теорем та елементами перевірки моделей.

Зв'язок роботи з науковими програмами, темами. Робота виконувалася в рамках наукових програм Інституту кібернетики ім. В.М. Глушкова “Розробка методів та засобів розв'язання логічних задач на алгебро-алгоритмічних моделях предметних областей”, шифр - ВГЕ.100.09, номер держреєстрації - 01940009539, “Розробка математичної теорії взаємодії компонент комп'ютерного середовища та її застосування у системі програмування АПС”, шифр - В.Ф.100.03, номер держреєстрації - 0198U000320, а також у рамках проекту VRS (Verіfіcatіon Requіrements Systems) "Верифікація вимог до систем", виконуваного в кампанії "Інформаційні програмні системи" разом з Інститутом кібернетики ім. В.М. Глушкова НАН України" і кампанією Motorola.

Мета і задачі дослідження. Основна мета дослідження - створення технології роботи з вимогами для телекомунікаційних систем, що мають велику кількість станів. Побудова формальних специфікацій за неформальними вимогами, їх верифікація, генерація набору тестів, синтез неповної архітектурної моделі і перевірка динамічних властивостей є складовою цієї технології. Задачі полягали в розробці та дослідженні формалізмів, що описують вимоги, побудові алгоритмів для відповідних етапів і створенні прототипів програмного забезпечення, що ілюструють роботу алгоритмів. Необхідно було

- визначити клас формальних специфікацій, для якого задачі технології вирішуються без експоненційного вибуху;

- сформулювати умови несуперечності і повноти;

- побудувати алгоритм символьної трасової генерації;

- побудувати алгоритм синтезу моделі за формальними специфікаціями;

- побудувати програму аналізу динамічних властивостей SDL-моделі, заданих за допомогою анотацій;

- створити прототипи програм верифікації формальних специфікацій і символьної генерації в системі інсерційного програмування;

- застосувати технологію для одного з телекомунікаційних проектів.

Наукова новизна отриманих результатів. Наукова новизна полягає в побудові технології для роботи з вимогами, представленими у вигляді інженерних специфікацій (мов MSC, SDL). Побудовано прототипи програм, що стали основою системи верифікації вимог, яка використовується в індустріальних проектах, що працюють з телекомунікаційними системами з великою кількістю станів. Виділено клас систем, вимоги до яких описуються за допомогою К-протоколів, і визначено алгоритми основних чотирьох задач технології: верифікація, генерація тестів, синтез моделі, аналіз динамічних властивостей. Відмінності даного класу визначаються можливостями рішення задач без експоненційного вибуху за часом. Таким чином, у роботі

- розроблена загальна технологія і методологія роботи з вимогами;

- визначений клас вимог у вигляді К-протоколів, що покривають великий клас телекомунікаційних задач, які вирішуються без експоненційного вибуху за часом;

- визначені властивості несуперечності і повноти для К-протоколів, а також методи їхньої перевірки;

- розроблені алгоритми прямої і зворотної символьної генерації множини символьних тестів;

- розроблений алгоритм синтезу неповної архітектурної моделі з множини К-протоколів;

- розроблений алгоритм перевірки динамічних властивостей, заданих за допомогою анотацій для моделей, які задані у вигляді SDL-специфікацій;

- розроблені прототипи програм символьної генерації тестів, програми перевірки властивостей SDL-специфікацій за допомогою анотацій.

Практична значимість результатів. Уперше системно запропоновано технологію роботи з вимогами у сучасних промислових проектах. Уведення процедур формалізації і верифікації вимог, генерації тестового набору, синтезу моделі й аналізу її динамічних властивостей дозволить значно скоротити час розробки і підвищити якість програмного продукту за рахунок виявлення помилок на ранніх стадіях розробки; генерації повного тестового набору, що покриває усі функціональності системи; автоматичного синтезу неповної архітектурної моделі; перевірки властивостей моделі на етапі збору вимог. Створена на основі досліджень система верифікації вимог використовувалась у 12 промислових проектах кампанії Motorola.

Особистий внесок здобувача. Усі результати, викладені в дисертації, отримані автором самостійно [1] на основі загальних результатів, опублікованих у спільних роботах [2-4]. У роботі [2] автором розроблена структура середовища для MSC-специфікацій, що не містять часу; в роботі [3] розроблена інcерційна програма - симулятор як основа програми перевірки динамічних властивостей, заданих за допомогою анотацій для моделей, записаних у вигляді SDL-специфікацій; у роботі [4] розроблено методи символьного моделювання за допомогою обернених предикатних перетворювачів, які використовуються в алгоритмах дисертації. Особисто автором також виділений клас формальних специфікацій, для якого задачі верифікації вирішуються без експоненційного вибуху, побудовані відповідні алгоритми і створені прототипи мовою АПЛАН і С/С++.

Апробація результатів дисертації. Наукові i практичні результати доповідались та обговорювались на Міжнародному семінар “Modelіng of Development Systems” (Київ, 2003), Міжнародній конференції "Теоретичні і прикладні аспекти побудови програмних систем" (Київ, 2004), Мiжнародному семiнарі "WITUL'04" (Ренн, Францiя, 2004), Міжнародній конференції, присвяченій 110-річчю винаходу радіо (Санкт-Петербург, 2005), Міжнародній конференції “SDL 2005: Model Driven” (Грімстад, Норвегія, 2005).

Публікації. Основні положення і результати опубліковані в 10 роботах, загальним обсягом 101 с., із них 5 - у наукових виданнях, 5 - у вигляді тез науково-практичних конференцій.

Структура дисертації. Дисертація складається із вступу, 6 розділів, післямови, висновків і списку літератури. Містить 3 таблиці, 15 рисунків, основний текст викладений на 132 сторінках. Список використаної літератури містить 64 джерела і викладений на 6 сторінках.

2. Основний зміст роботи

У вступі обґрунтовано актуальність теми, наукова новизна і необхідність вирішення проблеми забезпечення надійності та коректності функціонування систем з великою кількістю станів. Для цього визначається технологія роботи з вимогами і формулюються чотири основних задачі - верифікація, генерація трас, синтез моделі й аналіз. Оскільки вимоги визначають поведінку атрибутної транзиційної системи, то у сучасній літературі вже існують практичні й теоретичні результати. У вступі розглянуто класичні теорії паралелізму, а також подано огляд відповідних програмних систем.

У першому розділі роботи розглянуто стандартний процес збору й обробки вимог, а також місце цього процесу в загальному процесі розробки програмного забезпечення. Вимоги збираються у процесі спілкування з замовником, записуються у формальному вигляді і далі є основою для побудови програмного продукту. Формулюються також розглянуті в роботі задачі - верифікація вимог, генерація тестів, синтез неповної архітектурної моделі і перевірка динамічних властивостей у синтезованій моделі. Розглядаються сучасні інженерні мови специфікацій, у яких записуються вимоги. Наведено схему технології роботи з вимогами на основі рішень основних задач.

Другий розділ присвячено основним поняттям, що використовуються для формальних визначень базових протоколів і систем, заданих з їх допомогою. Основним є визначення атрибутної транзиційної системи , що представляє собою набір таких компонентів:

· S - множина станів;

· А - множина дій;

· - множина розмічених і нерозмічених (схованих) переходів;

· L - множина атрибутних розміток;

· - частково визначена функція розмітки станів.

При формалізації вимог використовуються абстракції великих атрибутних систем, стани яких розмічаються формулами деякої логічної мови, яку назвемо базовою. Ці формули виражають властивості розміток станів вихідної системи і можуть бути формулами мови числення предикатів першого та вищого порядків або формулами темпоральної логіки.

Визначаються також основні поняття теорії інсерційного програмування - агенти, середовища і функція занурення.

Агент - це розмічена транзиційна система, стани якої розглядаються з точністю до бісімуляційної еквівалентності. Агенти взаємодіють один з одним, виконуючи дії, що спостерігаються.

Стан агентів визначається його поводженням, відповідно еквівалентність агентів може бути визначена як еквівалентність виразів або рівнянь повної алгебри поводжень. Середовищем Е є агент над множиною дій середовища разом з функцією занурення. Функція Іns занурення в середовище є функція двох аргументів:

Іns(e,u) = e[u].

Перший аргумент е є поводженням середовища, другий - поводженням агента над множиною дій у заданому стані u. Результатом функції занурення є нове поводження даного середовища.

Для формального представлення вимог до системи використовується поняття базового протоколу. Базові протоколи застосовуються для подання вимог або специфікації систем на основі базової логічної мови. Система, специфікована базовими протоколами, являє собою середовище з зануреними в неї агентами.

Кожен базовий протокол є виразом вигляду , де x - список (типізованих) параметрів, і - формули базової мови, u - процес протоколу (цілком визначене поводження). Формула називається передумовою, а формула - постумовою базового протоколу. Протокол застосовується, якщо для деякого набору значень параметрів x істинна його передумова. Послідовність застосованих протоколів формує поводження системи. Протокол є конкретизованим, якщо в нього підставлені параметри.

Для кожної системи P базових протоколів як її реалізація буде однозначно визначена система S(P), породжена цими протоколами. Система S(P) - атрибутна система, що використовує формули базової мови як розмітку станів.

Для обчислення функції розмітки станів після застосування протоколу використовується предикатний перетворювач - перетворення, визначене на формулах базової мови.

У третьому розділі розглядається спеціальний клас базових протоколів як окремий випадок конкретних базових протоколів. Цей клас можна визначити як клас асинхронних імперативних базових протоколів з одним ключовим агентом. Базові протоколи зазначеного класу називаються К-протоколами.

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

Передумова К-протоколу b має вигляд , де а - ім'я ключового агента типу Т, що бере участь у протоколі, u - його стан, F - логічний вираз, побудований за допомогою логічних зв'язок, рівностей і нерівностей з атрибутів середовища і ключового агента. Процес proc(b) протоколу b являє собою послідовність дій, виконуваних ключовим агентом. Постумова post(b) базового протоколу b є кон'юнкція , де - новий стан агента а; G - сукупність операторів присвоювання . Тут - атрибути середовища або ключового агента; - вирази відповідних типів, що також залежні тільки від атрибутів ключового агента.

У роботі наведено приклад системи, заданої за допомогою К-протоколів, який являє собою формалізацію систему POTS (Plaіn Old Telephone System), що визначає функціонування звичайної телефонної мережі.

Сформульовано достатні умови несуперечності і повноти для системи, заданої за допомогою базових К-протоколів. Верифікація вимог має на меті перевірку істинності цих умов на множині К-протоколів.

Для двох параметризованих K-протоколів

з тим самим ключовим агентом, ім'я якого входить вільно у протоколи, умова несуперечливості формально виражається у вигляді заперечення кон'юнкції формул, що виражають умови застосовності цих протоколів:

.

Два K-протоколи формально несуперечливі, якщо ця умова, названа умовою транзиційної несуперечливості, не може бути спростована.

Умова повноти для K-протоколів ключового агента типу T, що знаходиться в стані s, формулюється в такий спосіб:

,

де - всі передумови K-протоколів; - списки їхніх параметрів, крім загального імені ключового агента n; emptyq(n) - предикат, що приймає значення 1, якщо в черзі немає повідомлень.

У четвертому розділі розглядається задача побудови набору трас за множиною К-протоколів. Траса розглядається як множина процесів базових протоколів, отриманих із усіх можливих історій функціонування системи. При цьому фіксується початковий стан системи, що містить у собі стан середовища, і стани всіх занурених у неї агентів.

Генерація трас може бути організована як послідовний перебір усіх можливих варіантів застосувань базових протоколів шляхом руху по дереву поводження системи, виходячи з деяких початкових станів. Генерація трас керується набором фільтрів, що використовуються в алгоритмі генерації трас як вхідна інформація. Фільтри задають умови завершення траси, виключення станів та інші властивості, використання яких сприяє оптимізації множини генерованих трас.

Для того, щоб не прив'язуватися до конкретного оточення, що складається з великої кількості агентів, а також не розглядати всі можливі набори значень атрибутів, що представляють можливі початкові стани середовища, можна скористатися абстрактною моделлю середовища і символьною трасовою генерацією.

Зміна стану середовища у процесі символьної генерації визначається за допомогою прямого предикатного перетворювача, що має такий вигляд:

Далі описано алгоритм прямої символьної генерації, що дає можливість породжувати множину символьних трас, які потім можуть бути перетворені в тести підстановкою конкретних значень.

Саме тестування відбувається як вплив оточення на тестованого агента. У трасах вхідні повідомлення, що посилаються з оточення агентові, розглядаються як команди керування, а вихідні повідомлення агента - як його контрольована реакція. Послідовність повідомлень, що керують тестуванням та надсилаються із середовища до агента, та повідомлень, що контролюються середовищем і які надсилаються агенту, є тестом.

Крім фільтрів, в алгоритмі використовується критерій покриття базових протоколів як умова закінчення процесу генерації тестів. Як такий критерій може бути розглянуте однократне покриття всіх протоколів.

Інший підхід до генерації трас складається в зворотному проходженні траси за допомогою зворотного предикатного перетворювача, що визначається в такий спосіб:

.

Поняття зворотного предикатного перетворювача використовується у відповідному алгоритмі генерації трас за допомогою фільтра факторизації станів агента.

Критерію однократного покриття усіх вимог може бути недостатньо, щоб створити вичерпний тестовий набір, тому що він не буде містити всіх поводжень і змін всіх атрибутів. З іншого боку, використання більш точних критеріїв покриття призводить до "експоненційного вибуху" кількості трас, необхідних для виконання такого критерію. Істотне зменшення кількості трас можна одержати шляхом факторизації простору станів агента (розбивки цього простору на класи), побудови повного набору трас усередині кожного з класів, а потім зв'язування класів з початковими і заключними станами системи невеликим числом трас.

Далі в розділі розглядається побудова алгоритму породження трас за допомогою фільтра факторизації, а також наводиться приклад роботи алгоритму на системі функціонування телефонної мережі.

У п'ятому розділі розглядається задача синтезу моделі за множиною вимог, представлених у вигляді К-протоколів. Побудовано алгоритм, входом якого є множина К-протоколів, а виходом - модель, представлена у вигляді SDL-системи. Алгоритм полягає у перетворенні компонентів К-протоколів у компоненти SDL-сис-теми. Для цього застосовуються наступні перетворення:

– визначення системи, процесів, каналів, сигналів, типів даних та змінних;

– визначення груп протоколів, що знаходяться в одному стані;

– визначення переходів для протоколів, що містять предикат в передумові;

– визначення переходів для незалежних та мішаних протоколів.

У шостому розділі розглянута перевірка динамічних властивостей SDL-моделі, представлених за допомогою анотацій. Як приклади таких властивостей можуть розглядатися властивості "safetу" (щось "погане" ніколи не відбудеться) і "lіveness" (щось "гарне" повинно колись відбутися).

Для реалізації програми перевірки динамічних властивостей використовується техніка інсерційного програмування. SDL-система є багаторівневим середовищем із зануреними в неї агентами - блоками системи. У свою чергу блоки є середовищем для процесів SDL-системи, а самі процеси - агентами. Для такої багаторівневої конструкції будується функція занурення, що фактично моделює роботу SDL-системи.

Для відображення динамічних властивостей формулюються анотації - деякі логічні вирази, що використовують формули першого порядку, атомарними виразами яких є константи та імена локальних змінних SDL-процесу. Дозволяється використання предикатів рівності (=) і нерівностей (>, <, >=, <=), аргументами яких є арифметичні лінійні комбінації змінних.

Анотації перевіряються на кожному кроці симуляції, що дозволяє доводити або спростовувати динамічні властивості, перевіряти досяжність визначених класів станів, одержувати поведінкові траси, що призводять до "гарних" або "поганих" випадків. Для доказу істинності формул першого порядку використовувалася доказова машина, побудована на базі APS, яка заснована на алгоритмі очевидності. Для роботи з арифметичними виразами використовувався лінійний вирішувач (lіnear solver), заснований на алгоритмі елімінації кванторів.

У післямові описується система верифікації вимог, у якій реалізовані вищеописані алгоритми. Система складається з наступних компонентів:

- програма перевірки транзиційної несуперечливості і повноти системи базових протоколів;

- програма генерації тестових сценаріїв з множини базових протоколів;

- програма перевірки сумісності MSC-сценаріїв і базових протоколів, а також доказ анотацій в розмічених MSC-діаграмах;

- програма для доказу властивостей анотованих SDL-специфікацій;

- графічна оболонка для підготовки даних системи VRS у вигляді базових протоколів, специфікованих MSC-діаграмами.

Висновки

У дисертаційній роботі отримані наступні результати:

1. Сформульовано технологію роботи з вимогами до інтерактивних систем. Вимоги формалізуються у вигляді базових протоколів, що можуть бути записані у формі діаграм однією з інженерних мов - MSC, SDL, UML. Сформульовано чотири основні задачі роботи з вимогами - верифікація, генерація тестів, синтез моделі, аналіз властивостей. Представлено схему використання результатів даних задач у загальному процесі створення програмного забезпечення. Використання даної технології забезпечить скорочення циклу розробки програмного забезпечення і підвищення якості програмного забезпечення за рахунок виявлення помилок на стадії збору вимог, автоматичної генерації тестового набору, автоматичним синтезом неповної архітектурної моделі продукту, перевірки динамічних властивостей моделі.

2. Виділено клас K-протоколів як клас, що покриває основну множину телекомунікаційних задач, і в якому задачі верифікації, аналізу та тестування вирішуються зі значним зниженням рівня експоненційного вибуху. Це відбувається за рахунок виключення паралелізму у функціонуванні всіх агентів. Задачі розглядаються стосовно одного ключового агента, що є тестований.

3. Сформульовано властивості несуперечливості і повноти для системи, заданої за допомогою К-протоколів. Доказ даних властивостей забезпечить відсутність таких помилок, як недетерміноване поводження або тупикові стани.

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

5. Сформульовано різні критерії покриття вимог тестовими наборами. Зокрема, одним із критеріїв є використання факторизації множини станів агента, що дозволяє значно скоротити набір тестів, необхідний для тестування ключового агента. Це досягається за допомогою конструювання трас із представників класів, у яких окремо будується повний набір трас методом зворотного символьного моделювання. Даний критерій гарантує повне покриття вимог і поводжень усередині кожного класу.

6. Побудовано алгоритм синтезу неповної архітектурної моделі, представленої у вигляді SDL-системи, з множини К-протоколів. Використання даного алгоритму може скоротити фазу розробки, а також запобігти частині помилок на етапі кодування.

7. Розроблено програму перевірки динамічних властивостей SDL-моделі, що формулюються за допомогою анотацій. Програма розроблена методом інсерційного програмування і дозволяє перевірити правильність властивостей моделі за допомогою моделювання і звертання до доказової машини.

8. Створено прототипи програм роботи з вимогами:

- програма підготовки вимог у вигляді формальних специфікацій за допомогою редактора MSC-діаграм;

- програма перевірки несуперечності і повноти системи вимог, заданих у вигляді формальних специфікацій;

- програма символьного моделювання і породження тестових наборів із заданих формальних специфікацій;

- програма перевірки динамічних властивостей SDL-моделей.

9. Створені автором прототипи є основою системи верифікації вимог, розробленої і впровадженої для роботи з вимогами у промислових телекомунікаційних моделях у кампанії Motorola, а також у кампанії "Інформаційні програмні системи". Результати використання системи викладені в таблиці.

Результати використання системи

Проект	Кількість вимог	Кількість протоколів	Покриття, %	Кількість помилок	Вартість (людино-тижні)
1	400	127	50	11	5.5
2	200	70	100	10	5.6
3	730	192	100	18	20.0
4	624	56	20	8	5.5
5	323	219	100	38	3.0
6	116	42	60	3	0.7

Основні праці

1. Летичевский А.А. / Об одном классе базовых протоколов // Проблемы программирования. - 2005. - № 4. - С. 82-97.

2. Semantics of timed MSC language / A.A. Letichevsky, J.V. Kapitonova, A.A. Letichevsky Jr. et all. // Кибернетика и системный анализ. - 2002. - № 4. - С. 3-14.

3. Инсерционное программирование / А.А. Летичевский, Ю.В. Капитонова, А.А. Летичевский (мл.) и др.// Там же. - 2003. - № 1. - С. 19-32.

4. Спецификация систем с помощью базовых протоколов / А.А. Летичевский, Ю.В. Капитонова, А.А. Летичевский (мл.) и др. // Там же. - 2005. - № 4. - С. 3-21.

5. Basic Protocols, Message Sequence Charts, and theVerification of Requirements Specifications / A.A. Letichevsky, J.K. Kapitonova, A.A. Letichevsky Jr. et all. // Proc. Intern. Workshop, WITUL'04, Rennes (France). - 2004. - P. 30-38.

6. Летичевський О.О. / Профілювання АПЛАН-програм // Проблемы программирования. - 2002. - № 3-4. - С. 98-103.

7. Insertion Programming and System Simulation / A.A. Letichevsky, J.K. Kapitonova, A.A. Letichevsky Jr. // Proc. XXVI Intern. Workshop on Modeling of Developing Systems. - Kiev, Ukraine, 2003. - Р. 19-20.

8. Tools For Requirements Capturing Based on the Technology Of Basic Protocols / Baranov S., Kapitonova J., Letichevsky A. Jr. et all // Proc. of St.Petersburg IEEE Chapters. - St. Petersburg, 2005. - С. 92-97.

9. Вишемирський В.В., Летичевський О.О. / Глобальна база знань в системах автоматичного доведення // Тези доп. Міжнар. конф. “Теоретичні та прикладні аспекти побудови програмних систем” TAAPSD'2004. - К. 2004. - С. 31-35.

10. Semantics of Message Sequenc Charts. / A.A. Letichevsky, J.K. Kapitonova, A.A. Letichevsky Jr. et all // Proc. 12 the Intern. SDL Forum, Grimstad, Norway. - 2005. - C. 117-132.

Размещено на Allbest.ru

...