Аннотация

Аннотация: Требования в нормативных документах часто задаются на естественном языке, поэтому автоматический поиск противоречий между ними затруднён. Кроме того, наличие противоречия может зависят от версии документа, режима работы объекта, исключений и приоритетов других требований. Цель статьи — определить требования к формальной модели, пригодной для автоматизированного выявления таких противоречий, и предложить модель на основе этих требований. В работе выполнен сравнительный анализ нормативных логик, временных логик, моделей ориентированных на цели, и специализированных нормативных языков. Основной результат — формализм DDL-LTLf, в котором нормы представлены как временные обязательства с исключениями и приоритетами, а задача поиска противоречий сведена к SATпроверке. Научная новизна состоит в объединении логики норм с исключениями и временной логики конечных трасс в единой семантике победивших норм и в доказанном булевом кодировании этой семантики. Практическая значимость подхода заключается в возможности использовать его как слой промежуточного представления требований между текстом нормативного документа и решателем, что позволяет выявлять реальные конфликты нормативных требований.