Методы верификации программного обеспечения

3.5.2. Мониторинг формальных свойств ПО 
Мониторинг формальных свойств ПО (для этой области используется два 
английских термина — runtime verification и passive testing) стал развиваться как 
отдельное направление исследований в конце 1990-х годов. В основе этого подхода 
лежит фиксация формальных свойств ПО, которые необходимо проверить и 
встраивание их проверок в систему мониторинга. В дальнейшем выполняется 
мониторинг ПО, в ходе которого контролируются и выделенные свойства. 
В публикациях упоминаются следующие методы мониторинга формальных 
свойств ПО. 

---

92 

Использующие описание свойств с помощью обычных и временных логик 
(см. [277,278]). Подобные техники осуществляют контроль свойств, записанных 
в виде формул временных логик, с помощью записи событий, происходящих в 
работающем ПО и анализа возникающих трасс. Один из инструментов, 
использующих такие техники — Temporal Rover [279,280]. 

Использующие описание свойств в виде систем переходов или автоматов 
(например, [281,282]). В этих техниках трасса анализируется не на выполнение 
некоторых формул, а на согласованность с заданной автоматной моделью 
правильного поведения. 

Использующие программные контракты (например, [283-285]). В рамках таких 
подходов корректность поведения системы проверяется во время ее работы с 
помощью оракулов на базе программных контрактов, внедренных в систему 
мониторинга. 
Более детальный обзор инструментов мониторинга формальных свойств можно 
найти в [286]. Пока методы мониторинга формальных свойств используются не в 
исследовательских целях достаточно редко, в основном, для мониторинга небольших 
критических приложений. Так, NASA применяет несколько таких инструментов, в том 
числе, разработанный силами собственных сотрудников Java PathExplorer [287], для 
верификации систем управления спутниковыми системами.