Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1341642, author = {Andersen, Jesper R. and Andersen, Nicklas and Enevoldsen, Soeren and Hansen, Mathias M. and Larsen, Kim G. and Olesen, Simon R. and Srba, Jiří and Wortmann, Jacob K.}, address = {Netherlands}, booktitle = {Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15)}, doi = {http://dx.doi.org/10.1007/978-3-319-25150-9_33}, keywords = {model checking; verification; concurrency workbench; tool; bisimulation}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Netherlands}, isbn = {978-3-319-25149-3}, pages = {573-582}, publisher = {Springer}, title = {CAAL: Concurrency Workbench, Aalborg Edition}, url = {http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33}, year = {2015} }
TY - JOUR ID - 1341642 AU - Andersen, Jesper R. - Andersen, Nicklas - Enevoldsen, Soeren - Hansen, Mathias M. - Larsen, Kim G. - Olesen, Simon R. - Srba, Jiří - Wortmann, Jacob K. PY - 2015 TI - CAAL: Concurrency Workbench, Aalborg Edition PB - Springer CY - Netherlands SN - 9783319251493 KW - model checking KW - verification KW - concurrency workbench KW - tool KW - bisimulation UR - http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33 L2 - http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33 N2 - We present the first official release of CAAL, a web-based tool for modelling and verification of concurrent processes. The tool is primarily designed for educational purposes and it supports the classical process algebra CCS together with its timed extension TCCS. It allows to compare processes with respect to a range of strong/weak and timed/untimed equivalences and preorders (bisimulation, simulation and traces) and supports model checking of CCS/TCCS processes against recursively defined formulae of Hennessy-Milner logic. The tool offers a graphical visualizer for displaying labelled transition systems, including their minimization up to strong/weak bisimulation, and process behaviour can be examined by playing (bi)simulation and model checking games or via the generation of distinguishing formulae for non-equivalent processes. We describe the modelling and analysis features of CAAL, discuss the underlying verification algorithms and show a typical example of a use in the classroom environment. ER -
ANDERSEN, Jesper R., Nicklas ANDERSEN, Soeren ENEVOLDSEN, Mathias M. HANSEN, Kim G. LARSEN, Simon R. OLESEN, Jiří SRBA a Jacob K. WORTMANN. CAAL: Concurrency Workbench, Aalborg Edition. In \textit{Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15)}. Netherlands: Springer, 2015, s.~573-582. ISBN~978-3-319-25149-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-25150-9\_{}33.
|