Том 17, № 4 (2010)
Оригинальные статьи
17-26 402
Аннотация
Предлагается метод подготовки тестовых данных, обеспечивающих определенный уровень покрытия требований для функционального тестирования. Использование метода упрощает поддержание в непротиворечивом состоянии конфигурации данных жизненного цикла проекта, включающей в себя требования, программный код и сгенерированные тесты. Вводится классификация дефектов программного обеспечения. Предлагается подход к формализации анализа требований и реализации тестируемой системы, основанный на представлении разбиения на классы эквивалентности в виде системы логических уравнений. Предложен приблизительный метод решения получаемых уравнений. Обсуждается применимость подхода в реальных процессах промышленных проектов.
27-40 476
Аннотация
Статья посвящена тестированию соответствия (конформности) реализации требованиям спецификации. Идея безопасного тестирования предложена авторами для конформности, основанной на трассах наблюдений. Эта идея распространяется на случай (слабой) симуляции, основанной на соответствии состояний реализации и спецификации. Предлагается теория безопасной симуляции для систем с отказами и разрушением. Обсуждаются вопросы полноты тестирования и достаточные условия существования полного набора тестов. Предлагается алгоритм полного тестирования для практического применения, опирающийся на некоторые ограничения на реализацию и спецификацию.
41-51 426
Аннотация
Рассматриваются вероятностные системы взаимодействующих недетерминированных интеллектуальных агентов. Состояниями агентов в таких системах являются вероятностные базы данных (фактов), а их действия управляются вероятностными логическими программами. Кроме того, каналы взаимодействий между агентами также являются вероятностными. Показано, как таким системам за полиномиальное время могут быть сопоставлены моделирующие их конечные Марковские процессы принятия решений. Это позволяет перенести известные результаты о верификации динамических свойств конечных Марковских процессов на вероятностные мультиагентные системы рассматриваемого типа.
52-59 478
Аннотация
Предложено эффективное символьное представление распределенных систем, определяемых линейными функциями над целочисленными переменными.
60-69 452
Аннотация
Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как тйповые кванторы. Язык LF содержит всего два логических символа - для каждого и существует, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.
70-77 468
Аннотация
Рассматривается способ статического семантического анализа исходных кодов программы на стадии ее компиляции с целью повышения качества исходного кода. В качестве способа реализации такого семантического анализа предлагается унифицированная интеграция в компиляторы языка Java для получения полного доступа к синтаксическому дереву (AST) компилируемых программ после этапа семантического анализа. Для обеспечения унификации реализованы общие интерфейсы для работы с синтаксическим деревом и адаптеры к реализациям синтаксических деревьев в компиляторах Sun/Oracle javac и Eclipse Compiler for Java (ecj). Выбранный способ обеспечил прозрачную интеграцию со средами разработки Eclipse и Netbeans без необходимости установки каких-либо расширений данных сред. Разработанный метод демонстрируется на некоторых примерах верификации программ.
78-87 563
Аннотация
Показано, что метод адаптивной редукции симметричных моделей (ASR), предложенный в статье [9] для сокращения пространства поиска при решении проблемы достижимости в моделях программ, может быть с равным успехом применен для проверки выполнимости формул логики линейного времени ILTL на конечных моделях распределённых программ. Задача проверки выполнимости формул ILTL сводится к задаче проверки пустоты автомата Бюхи, решаемой при помощи комбинированного алгоритма, в котором процедура двойного поиска в глубину (DDFS) сочетается с последовательным уточнением пространства поиска на основе принципов ASR.
88-100 445
Аннотация
Представлена расширяемая мультиязыковая система анализа и верификации СПЕКТР, разрабатываемая в рамках одноименного проекта, и показаны перспективы ее использования на примере верификации C-программ. Проект СПЕКТР направлен на создание нового интегрированного подхода к верификации императивных программ, который позволяет интегрировать, унифицировать и комбинировать методы и техники верификации императивных программ, накапливать и использовать знания о них. Особенностью подхода является использование специализированного языка выполнимых спецификаций Atoment для разработки средств верификации программ, который позволяет представить в едином унифицированном формате как методы и техники верификации, так и данные для них (программные модели, аннотации, логические формулы). C-компонента системы СПЕКТР использует двухуровневый метод верификации C-программ. Этот метод является хорошей иллюстрацией интегрированного подхода, поскольку он обеспечивает комплексную верификацию C-программ, базирующуюся на комбинации операционного, аксиоматического и трансформационного подходов.
101-110 503
Аннотация
Дедуктивная верификация и синтез программ двоичного сложения проводятся на базе системы правил доказательства корректности для операторов языка предикатного программирования P. В работе представлены ключевые фрагменты процесса верификации и синтеза программ сумматоров. Условия корректности программ транслировались на язык спецификаций системы автоматического доказательства PVS. Доказательство на PVS оказалось на порядок более трудоемким процессом по сравнению с обычным программированием. Однако в режиме синтеза построение теорий и доказательство на PVS проще и быстрее по сравнению с верификацией.
111-124 474
Аннотация
Верифицирующий компилятор - это системная компьютерная программа, которая транслирует написанные человеком программы с языка высокого уровня в эквивалентные исполнимые программы и, кроме того, доказывает (верифицирует) специфицированные человеком математические утверждения о свойствах транслируемых программ. Цель проекта F@BOOL@ - разработка понятного для пользователей, компактного и переносимого верифицирующего компилятора аннотированных вычислительных программ, использующего эффективные и достоверные автоматические SAT-решатели в качестве средств автоматической проверки истинности условий корректности (вместо средств полуавтоматического доказательства). В период с 2006 по 2009 гг. в проекте F@BOOL@ использовался SAT-решатель zChaff. С его помощью были выполнены первые эксперименты по верификации простых программ на Mini-NIL: программы обмена переменных своими значениями, проверки троек целых чисел быть длинами сторон равностороннего или равнобедренного треугольника, и поиска одной фальшивой среди 15 монет с использованием чашечных весов. В работе рассказано об основных идеях проекта F@BOOL@ и приведены детали эксперимента по верификации программы, решающей головоломку о монетах.
125-136 409
Аннотация
Рассматривается проблема включения метода формальной верификации - проверки модели - в процесс проектирования сложных распределенных программных систем. В качестве центрального объекта проектирования предлагается использовать платформенно-независимую модель, которая строится на основе ядра системы, отвечающего за логическое управление всей системой как единым целым. Подход позволяет повысить качество разрабатываемого программного обеспечения и гарантировать соответствие задаваемой спецификации. Предлагаемая методика опробована на реальной системе управления энергоснабжением судна.
ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)
ISSN 2313-5417 (Online)