- Tytuł:
- Model checking processes specified in join-calculus algebra
- Autorzy:
-
Maludziński, S.
Dobrowolski, G. - Powiązania:
- https://bibliotekanauki.pl/articles/305715.pdf
- Data publikacji:
- 2014
- Wydawca:
- Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
- Tematy:
-
join-calculus
model checking
formal methods
automatic software verification - Opis:
- This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra, with its operational semantics defined by a chemical abstract machine, serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, allowing for the examination of more complex systems. The described model checker is a proof of concept for the utilization of new methodologies of formal system specification and verification in software engineering practice.
- Źródło:
-
Computer Science; 2014, 15 (1); 61-74
1508-2806
2300-7036 - Pojawia się w:
- Computer Science
- Dostawca treści:
- Biblioteka Nauki
Artykuł