Abstract This paper reports on an effort to build a tool for modeling, manipulation, and analysis of concurrent systems. The tool implements the CCS process language and can build labeled transition systems in Aldebaran format from CCS expressions. Furthermore, it can be used to reduce the state space of a labeled transition system and to check whether two labeled transition systems exhibit the same behaviour, using two behavioural equivalences: strong and weak bisimulation equivalence. The tool has the functionality needed to perform modeling, specification, and verification, illustrated on one classical example in the concurrency theory: the Alternating Bit Protocol.
/
© Association for Information and Communication Technologies www.ict-act.org Developed by tdelev