Detail publikace
Verifying Concurrent Programs Using Contracts
Ferreira Carla (UNL)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Lourenco Joao (UNL)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Sousa Diogo J. (UNL)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Tento článek se zabývá kontrakty pro paralelní programy, které umožňují definovat a zkoumat očekávanou atomicitu provádění metod nebo volání služeb v paralelních programech. Kontrakty mohou být buď získávány automaticky ze zdrojových kódů nebo poskytovány přímo vývojáři knihoven nebo modulů softwaru tak, aby vyjadřovaly očekávané použití v paralelním běhu. Ve článku nejprve rozšiřujeme pojem kontraktů v paralelismu několika způsoby zlepšující jejich vyjadřovací sílu a rozšiřující jejich aplikovatelnost v praxi. Dále navrhujeme dvě doplňující analýzy, statickou a dynamickou, k verifikaci programů s ohledem na rozšířené kontrakty. Implementovali jsme oba přístupy analýzy programů a dosáhli slibných experimentálních výsledků při aplikaci na různých programech, přičemž u reálných programů jsme pomocí našeho přístupu odhalili dosut neznámé chyby.
@INPROCEEDINGS{FITPUB11510, author = "J. Ricardo Dias and Carla Ferreira and Jan Fiedor and Joao Lourenco and Ale\v{s} Smr\v{c}ka and J. Diogo Sousa and Tom\'{a}\v{s} Vojnar", title = "Verifying Concurrent Programs Using Contracts", pages = "196--206", booktitle = "2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)", year = 2017, location = "Tokyo, JP", publisher = "Institute of Electrical and Electronics Engineers", ISBN = "978-1-5090-6032-0", doi = "10.1109/ICST.2017.25", language = "english", url = "https://www.fit.vut.cz/research/publication/11510" }