CAAL: Concurrency Workbench, Aalborg Edition

D 2015

CAAL: Concurrency Workbench, Aalborg Edition

ANDERSEN, Jesper R., Nicklas ANDERSEN, Soeren ENEVOLDSEN, Mathias M. HANSEN, Kim G. LARSEN et. al.

Basic information

Original name

CAAL: Concurrency Workbench, Aalborg Edition

Authors

ANDERSEN, Jesper R. (208 Denmark), Nicklas ANDERSEN (208 Denmark), Soeren ENEVOLDSEN (208 Denmark), Mathias M. HANSEN (208 Denmark), Kim G. LARSEN (208 Denmark), Simon R. OLESEN (208 Denmark), Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution) and Jacob K. WORTMANN (208 Denmark)

Edition

Netherlands, Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15), p. 573-582, 10 pp. 2015

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00087229

Organization unit

Faculty of Informatics

ISBN

978-3-319-25149-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-25150-9_33

UT WoS

000366212700033

Keywords in English

model checking; verification; concurrency workbench; tool; bisimulation

Abstract

V originále

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.

Citovat

ANDERSEN, Jesper R., Nicklas ANDERSEN, Soeren ENEVOLDSEN, Mathias M. HANSEN, Kim G. LARSEN, Simon R. OLESEN, Jiří SRBA and Jacob K. WORTMANN. CAAL: Concurrency Workbench, Aalborg Edition. In Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15). Netherlands: Springer, 2015, p. 573-582. ISBN 978-3-319-25149-3. Available from: https://dx.doi.org/10.1007/978-3-319-25150-9_33.

@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 and 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, p.~573-582. ISBN~978-3-319-25149-3. Available from: https://dx.doi.org/10.1007/978-3-319-25150-9\_{}33.

Detailed Information on Publication Record