CAAL: Concurrency Workbench, Aalborg Edition

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F15%3A00087229" target="_blank" >RIV/00216224:14330/15:00087229 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-25150-9_33" target="_blank" >10.1007/978-3-319-25150-9_33</a>

Jazyk výsledku

angličtina

Název v původním jazyce

CAAL: Concurrency Workbench, Aalborg Edition

Popis výsledku v původním jazyce

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 ofHennessy-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

Název v anglickém jazyce

CAAL: Concurrency Workbench, Aalborg Edition

Popis výsledku anglicky

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 ofHennessy-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

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15)

ISBN

9783319251493

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

10

Strana od-do

573-582

Název nakladatele

Springer

Místo vydání

Netherlands

Místo konání akce

Cali, Colombia

Datum konání akce

1. 1. 2015

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000366212700033