Формальная проверка сроков
Мне известны различные формальные средства проверки для проверки свойств программ (например, средство проверки модели SPIN). Существуют ли какие-либо общие инструменты / методологии для проверки требований к синхронизации во встроенных системах реального времени? Например: "Этот алгоритм должен всегда завершаться в течение 50 мс". Как обычно проводится проверка такого типа?
2 ответа
Монотонный анализ скорости может быть полезен при определении того, является ли система запланированной, учитывая задержки активации и сроки выполнения всех задач. Существуют пакеты, которые могут помочь вам в подсчете чисел, но я думаю, что математика не ограничивается таблицей.
Кроме того, тип технического требования, которое вы упомянули, может быть трудно проверить. Даже если у вас есть возможность измерить количество времени, в течение которого алгоритм активен, часто невозможно протестировать все возможные сценарии, чтобы убедиться, что крайний срок никогда не превышается.
Что я видел в критически важных приложениях, таких как кардиостимуляторы и авионика, так это в том, чтобы спроектировать алгоритм так, чтобы он не превышал требуемый срок. Это может быть сделано либо ограничением объема данных, которые он может обработать за одну активацию, либо наличием самого времени функции и преждевременным завершением (и возвратом ошибки), если оно превышает крайний срок. Надеюсь, это поможет.
Существует инструмент (ы) UPPAAL, IF, набор инструментов для проверки моделей временных систем. Он основан на теории временных автоматов.