.png) |
| Источник: MIT |
Ученые Массачусетского технологического института адаптировали для программных систем функции Ляпунова, описывающие устойчивость динамической системы. Они названы так по имени великого русского математика и являются одной из основ теории управления. Простейший пример функции Ляпунова описывает движения маятника.
Авторы предлагают рассматривать компьютерную программу как набор правил перемещения в пространстве, определенном переменными программы и размещением в памяти ее команд. Любое состояние программы (набор значений переменных при выполнении очередной инструкции) — точка такого пространства. Критические ошибки исполнения, например деление на ноль или переполнение памяти, можно рассматривать как области этого пространства.
В таком контексте задача формальной верификации сводится к демонстрации того, что программа никогда не «заведет» свои переменные в зоны критических ошибок. Для этого исследователи предложили аналог функций Ляпунова, которые они назвали инвариантами Ляпунова. График функции Ляпунова похож на чашу, ее нижняя точка — состояние максимальной стабильности. Для программы нужно найти такой инвариант Ляпунова, чтобы начальные значения переменных находились на дне «чаши», а все опасные зоны — выше на стенках. В этом случае попадание в опасную зону будет равносильно тому, что маятник качнулся сильнее, чем в предыдущий раз.
