Podpora jazyku Promela v moderním IDE
| Název práce v češtině: | Podpora jazyku Promela v moderním IDE |
|---|---|
| Název v anglickém jazyce: | Promela Support in Modern IDE |
| Akademický rok vypsání: | 2025/2026 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 19.11.2025 |
| Datum zadání: | 24.11.2025 |
| Datum potvrzení stud. oddělením: | 25.11.2025 |
| Zásady pro vypracování |
| Jazyk Promela [1] patří k nejpoužívanějším jazykům pro modelování a verifikace chování počítačových systémů. Jedná se o vstupní jazyk verifikačního nástroje Spin, který je široce využíván nejen na akademické půdě, ale i v průmyslu.
V současné době nicméně neexistuje volně dostupné vývojové prostředí, které by podporovalo vyvíjení modelů v jazyku Promela a zároveň poskytovalo obvyklý komfort pro vývojáře, jako zvýrazňování syntaxe, možnost navigace v kódu a provádění verifikací a analýzu jejich výsledků. Cílem této bakalářské práce je zvolit vhodné vývojové prostředí, například [2,3], a navrhnout a implementovat do něj podporu pro vytváření a analýzu modelů v jazyku Promela (s použitím existujícího model checkeru Spin [1]). Implementované vlastnosti budou zahrnovat zejména zvýrazňování syntaxe, navigaci v kódu a spouštění verifikací, případně simulací modelu. |
| Seznam odborné literatury |
| [1] Gerald J. Holzmann: The Spin Model Checker: Primer and Reference Manual, 1st Edition, ISBN 978-0321228628, Addison-Wesley Professional, January 1, 2003
[2] The open source AI code editor: https://code.visualstudio.com/ [3] JetBrains IDE: https://www.jetbrains.com/ |