Улучшенный верифицирующий алгоритм для математической модели взаимных блокировок

Аннотация

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