Улучшенный верифицирующий алгоритм для математической модели взаимных блокировок
Автор: Свирин Илья Сергеевич, Силин Павел Александрович, Парфилов Иван Васильевич
Журнал: Сетевое научное издание «Системный анализ в науке и образовании» @journal-sanse
Статья в выпуске: 3, 2013 года.
Бесплатный доступ
В статье рассматривается алгоритм поиска взаимных блокировок в программном обеспечении на основе его модели. Введено понятие модели взаимных блокировок на основе теории графов, учитывающей понятия субъекта доступа, разделяемого ресурса и средства синхронизации. Приведен верифицирующий алгоритм, заключающийся в сведении систем линейных субъектов к ориентированным графам, вершинами которых являются операторы взаимодействия со средствами синхронизации, а ребра соответствуют соотношениям, возникающим между данными операторами в рамках системы субъектов. Приведено доказательство теорем, подтверждающих работоспособность предложенного алгоритма.
Верификация программного обеспечения, алгоритм верификации
Короткий адрес: https://sciup.org/14123232
IDR: 14123232
Список литературы Улучшенный верифицирующий алгоритм для математической модели взаимных блокировок
- Artho C., Biere A. Applying Static Analysis to Large-Scale, Multi-threaded Java Programs // 13th Australien Software Engineering Conference, August 2001. - IEEE Computer Society. - 2011. - Pp. 68-75.
- Bensalem S., Havelund K. Dynamic Deadlock Analysis of Multi-threaded Programs // Haifa Verification Conference, Springer, 2005. - Vol. 3875. - Pp. - 208-223.
- Detlefs D. L., Rustan K., Leino M., Nelson G., Saxe J. B. Extended Static Checking // Technical Report 159, Compaq Systems Research Center, Palo Alto, California, USA, 1998.
- Engler D., Ashcraft K. RacerX: Effective, Static Detection of Race Conditions and Deadlocks // Proceedings of the 19th ACM Symposium on Operating Systems Principles, October 2003. - Pp. 237-252.
- Havelund K., Pressburger T. Model Checking Java Programs using JavaPathFinder // International Journal on Software Tools for Technology Transfer, 2(4):366-381, April 2000. Special issue of STTT containing selected submissions to the 4th SPIN workshop. - Paris, France, 1998.
