ВКР ФИТ НГУ Разработка редактора спецификаций требований к управляющему ПО на языке EDTL

Создание среды разработки формальных спецификаций для верификации управляющего ПО

Актуальность формальных спецификаций требований для надежного управляющего ПО

Студенты ФИТ НГУ, работающие над темами формальной верификации, сталкиваются с отсутствием специализированных инструментов для спецификации требований к управляющему ПО как черному ящику. Система EDTL4CSRS (Event-Driven Temporal Logic for Control Software Requirements Specification) призвана решить эту проблему, предоставляя язык и среду разработки для формального описания свойств программного обеспечения.

Особую сложность представляет создание редактора, который объединяет выразительность темпоральной логики, ориентированной на события, с удобным интерфейсом для инженеров. Многие студенты недооценивают объем работ по разработке грамматики языка, реализации средств верификации спецификаций и интеграции с существующими системами разработки управляющего ПО. В этой статье мы представим комплексный подход к созданию такого редактора с практическими примерами на Java и Xtext.

Срочная помощь по вашей теме: Получите консультацию за 10 минут! Telegram: @Diplomit Телефон/WhatsApp: +7 (987) 915-99-32, Email: admin@diplom-it.ru

Оформите заказ онлайн: Заказать ВКР ФИТ НГУ

Архитектура системы EDTL4CSRS

Компоненты среды разработки спецификаций

Эффективная система спецификации требований должна включать следующие модули:

• Редактор EDTL-спецификаций — среда разработки с подсветкой синтаксиса
• Парсер и валидатор — анализ корректности спецификаций
• Генератор условий верификации — преобразование в форматы солверов
• Интегратор с poST-программами — связь спецификаций с реализацией
• Система визуализации — графическое представление спецификаций
• Менеджер проектов — организация наборов спецификаций

Разработка грамматики языка EDTL в Xtext

Формальное описание синтаксиса Event-Driven Temporal Logic

Рассмотрим грамматику языка EDTL для спецификации требований к управляющему ПО:

grammar ru.diplom.edtl.EDTLLanguage with org.eclipse.xtext.common.Terminals
generate edtlLanguage "http://www.diplom-it.ru/EDTLLanguage"
RequirementsSpecification:
    'REQUIREMENTS' 'FOR' systemName=ID
    '{'
        imports+=Import*
        signals+=SignalDeclaration*
        requirements+=Requirement+
    '}';
Import:
    'IMPORT' importedNamespace=QualifiedName;
SignalDeclaration:
    'SIGNAL' name=ID ':' type=SignalType ('=' initialValue=Expression)?;
SignalType:
    'BOOL' | 'INT' | 'REAL' | 'ENUM' '{' literals+=ID (',' literals+=ID)* '}';
Requirement:
    'REQUIREMENT' name=ID
    '{'
        description=Description
        scope=TemporalScope
        pattern=EventPattern
        (tags+=Tag)*
    '}';
Description:
    'DESCRIPTION' text=STRING;
TemporalScope:
    'GLOBAL' | 'INITIAL' | 'AFTER' event=EventExpression;
EventPattern:
    TriggerPattern | ResponsePattern | PreventionPattern | PersistencePattern;
TriggerPattern:
    'TRIGGER' trigger=EventExpression
    'RESPONSE' response=EventExpression
    ('WITHIN' timeout=TimeExpression)?;
ResponsePattern:
    'WHEN' condition=StateExpression
    'RESPONSE' response=EventExpression
    ('WITHIN' timeout=TimeExpression)?;
PreventionPattern:
    'PREVENT' event=EventExpression
    'WHEN' condition=StateExpression;
PersistencePattern:
    'MAINTAIN' condition=StateExpression
    'FOR' duration=TimeExpression;
EventExpression:
    SimpleEvent | CompositeEvent;
SimpleEvent:
    signal=[SignalDeclaration] (operator=ComparisonOperator value=Expression)?;
CompositeEvent:
    '(' left=EventExpression ')' operator=EventOperator right=EventExpression;
EventOperator:
    'AND' | 'OR' | 'THEN' | 'FOLLOWED_BY';
StateExpression:
    BooleanExpression;
TimeExpression:
    value=Number unit=TimeUnit;
TimeUnit:
    'ms' | 's' | 'min' | 'h';
// Пример спецификации требований к системе управления лифтом
REQUIREMENTS FOR ElevatorControlSystem {
    SIGNAL callButton: BOOL = false
    SIGNAL floorSensor: INT = 1
    SIGNAL doorOpen: BOOL = false
    SIGNAL doorClosed: BOOL = true
    SIGNAL moving: BOOL = false
    SIGNAL currentFloor: INT = 1
    REQUIREMENT DoorSafety {
        DESCRIPTION "Двери не должны открываться во время движения"
        SCOPE GLOBAL
        PREVENT doorOpen = true
        WHEN moving = true
    }
    REQUIREMENT CallResponse {
        DESCRIPTION "При нажатии кнопки вызова лифт должен приехать в течение 30 секунд"
        SCOPE GLOBAL
        TRIGGER callButton = true
        RESPONSE currentFloor = callButton.floor
        WITHIN 30 s
    }
    REQUIREMENT DoorOpenTime {
        DESCRIPTION "Двери должны оставаться открытыми не менее 5 секунд"
        SCOPE AFTER doorOpen = true
        MAINTAIN doorOpen = true
        FOR 5 s
    }
}

Реализация редактора с расширенными возможностями

Создание IDE для EDTL с автодополнением и валидацией

// Реализация кастомного редактора EDTL в Eclipse
public class EDTLEditor extends XtextEditor {
    @Override
    protected void initializeEditor() {
        super.initializeEditor();
        configureSyntaxHighlighting();
        configureContentAssist();
        configureErrorAnnotation();
    }
    private void configureSyntaxHighlighting() {
        IPreferenceStore store = getPreferenceStore();
        store.setDefault(EDTLHighlightingConfiguration.KEYWORD_ID, true);
        store.setDefault(EDTLHighlightingConfiguration.SIGNAL_ID, true);
        store.setDefault(EDTLHighlightingConfiguration.REQUIREMENT_ID, true);
        store.setDefault(EDTLHighlightingConfiguration.TIME_ID, true);
    }
    private void configureContentAssist() {
        IContentAssistProcessor processor = 
            new EDTLContentAssistProcessor();
        getSourceViewer().setContentAssistProcessor(
            processor, IDocument.DEFAULT_CONTENT_TYPE);
    }
}
// Специализированный валидатор для EDTL
public class EDTLValidator extends AbstractEDTLValidator {
    public static final String INVALID_TIMEOUT = "invalid_timeout";
    public static final String UNSATISFIABLE_REQUIREMENT = "unsatisfiable";
    @Check
    public void checkTimeoutValue(TimeExpression timeExpr) {
        if (timeExpr.getValue() <= 0) {
            error("Таймаут должен быть положительным числом", 
                  EDTLPackage.Literals.TIME_EXPRESSION__VALUE,
                  INVALID_TIMEOUT);
        }
    }
    @Check
    public void checkRequirementConsistency(Requirement requirement) {
        // Проверка выполнимости требования
        if (!isRequirementSatisfiable(requirement)) {
            warning("Требование может быть невыполнимым при заданных условиях",
                   EDTLPackage.Literals.REQUIREMENT__PATTERN,
                   UNSATISFIABLE_REQUIREMENT);
        }
    }
    @Check
    public void checkSignalUsage(SignalDeclaration signal) {
        // Проверка, что сигнал используется хотя бы в одном требовании
        if (!isSignalUsed(signal)) {
            warning("Сигнал объявлен, но не используется в требованиях",
                   EDTLPackage.Literals.SIGNAL_DECLARATION__NAME,
                   "unused_signal");
        }
    }
}
// Провайдер контент-ассиста для автодополнения
public class EDTLContentAssistProcessor extends AbstractContentAssistProcessor {
    @Override
    public ICompletionProposal[] computeCompletionProposals(
            ITextViewer viewer, int offset) {
        List<ICompletionProposal> proposals = new ArrayList<>();
        // Предложения ключевых слов
        proposals.addAll(createKeywordProposals(viewer, offset));
        // Предложения сигналов
        proposals.addAll(createSignalProposals(viewer, offset));
        // Предложения шаблонов требований
        proposals.addAll(createPatternTemplates(viewer, offset));
        return proposals.toArray(new ICompletionProposal[0]);
    }
    private List<ICompletionProposal> createPatternTemplates(
            ITextViewer viewer, int offset) {
        List<ICompletionProposal> templates = new ArrayList<>();
        // Шаблон для триггер-ответных требований
        String triggerTemplate = 
            "REQUIREMENT ${name} {\n" +
            "    DESCRIPTION \"${description}\"\n" +
            "    SCOPE GLOBAL\n" +
            "    TRIGGER ${event}\n" +
            "    RESPONSE ${response}\n" +
            "    WITHIN ${timeout}\n" +
            "}";
        templates.add(createTemplateProposal("Trigger-Response Pattern", 
            triggerTemplate, "Шаблон требования типа триггер-ответ", offset));
        return templates;
    }
}

Интеграция с poST-программами для верификации

Связь формальных спецификаций с реализацией

Почему 150+ студентов выбрали нас в 2025 году

• Оформление по всем требованиям вашего вуза (мы изучаем 30+ методичек ежегодно)
• Поддержка до защиты включена в стоимость
• Доработки без ограничения сроков
• Гарантия уникальности 90%+ по системе "Антиплагиат.ВУЗ"

Расширенные возможности редактора

Дополнительные функции для продуктивной работы

Функция 1: Интеллектуальное автодополнение

Реализация: Контекстно-зависимые предложения на основе грамматики EDTL и используемых сигналов

Функция 2: Визуализация временных диаграмм

Реализация: Автоматическое построение временных диаграмм для паттернов требований

Функция 3: Статический анализ спецификаций

Реализация: Проверка непротиворечивости и полноты набора требований

Пример комплексной спецификации требований

Спецификация для системы управления температурой

REQUIREMENTS FOR TemperatureControlSystem {
    SIGNAL temperature: REAL = 20.0
    SIGNAL setpoint: REAL = 22.0
    SIGNAL heaterOn: BOOL = false
    SIGNAL coolerOn: BOOL = false
    SIGNAL emergencyStop: BOOL = false
    REQUIREMENT TemperatureStability {
        DESCRIPTION "Температура должна поддерживаться вблизи уставки"
        SCOPE GLOBAL
        MAINTAIN temperature >= setpoint - 1.0 AND temperature <= setpoint + 1.0
        FOR 10 min
    }
    REQUIREMENT HeaterControl {
        DESCRIPTION "Обогреватель должен включаться при температуре ниже уставки"
        SCOPE GLOBAL
        WHEN temperature < setpoint - 0.5
        RESPONSE heaterOn = true
        WITHIN 5 s
    }
    REQUIREMENT CoolerControl {
        DESCRIPTION "Охладитель должен включаться при температуре выше уставки"
        SCOPE GLOBAL
        WHEN temperature > setpoint + 0.5
        RESPONSE coolerOn = true
        WITHIN 5 s
    }
    REQUIREMENT MutualExclusion {
        DESCRIPTION "Обогреватель и охладитель не должны работать одновременно"
        SCOPE GLOBAL
        PREVENT heaterOn = true AND coolerOn = true
    }
    REQUIREMENT EmergencyShutdown {
        DESCRIPTION "При аварийной остановке все системы должны выключиться"
        SCOPE GLOBAL
        TRIGGER emergencyStop = true
        RESPONSE heaterOn = false AND coolerOn = false
        WITHIN 1 s
    }
    REQUIREMENT OverheatProtection {
        DESCRIPTION "При превышении температуры 40°C должна сработать защита"
        SCOPE GLOBAL
        WHEN temperature > 40.0
        RESPONSE emergencyStop = true
        WITHIN 500 ms
    }
}

Методика использования редактора в учебном процессе

Интеграция с курсами по формальным методам

Для эффективного использования редактора в образовательных целях:

1. Поэтапное изучение EDTL — от простых к сложным конструкциям
2. Практические задания — спецификация требований для реальных систем
3. Верификация примеров — проверка корректности спецификаций
4. Проектная работа — разработка полного набора требований
5. Сравнительный анализ — оценка различных подходов к спецификации

Примеры учебных заданий можно найти в нашем разделе выполненных работ.

Срочная помощь по вашей теме: Получите консультацию за 10 минут! Telegram: @Diplomit Телефон/WhatsApp: +7 (987) 915-99-32, Email: admin@diplom-it.ru

Оформите заказ онлайн: Заказать ВКР ФИТ НГУ

Заключение

Разработка редактора спецификаций требований к управляющему ПО на языке EDTL представляет собой комплексную задачу, требующую интеграции знаний в области языково-ориентированного программирования, формальных методов и инженерии требований. Система EDTL4CSRS позволяет специфицировать свойства ПО как черного ящика, обеспечивая формальную основу для верификации корректности управляющих программ.

Если вы столкнулись со сложностями в разработке грамматики Xtext, реализации средств верификации или интеграции с poST-программами — обратитесь к нашим специалистам. Мы обеспечим не только качественное выполнение работы, но и полное соответствие гарантиям и требованиям ФИТ НГУ.

Дополнительные материалы для изучения:

• Актуальные темы дипломных работ по прикладной информатике
• Современные направления в информатике для ВКР
• Темы от классических алгоритмов до современных трендов

Наши услуги и гарантии:

• Условия работы и как сделать заказ
• Наши гарантии
• Отзывы наших клиентов
• Примеры выполненных работ