ABCD: A User-Friendly Language for Formal Modelling and Analysis

摘要

This paper presents an algebra of coloured Petri nets called the Asynchronous Box Calculus with Data, or ABCD for short. ABCD allows to model complex systems using a user-friendly and high-level syntax. In particular, parts of the model can be directly programmed in Python [21], which allows to embed complex computation and data values within a model. A compiler for ABCD is shipped with the toolkit SNAKES [16,18] and ABCD has been used for years, which is quickly surveyed. This paper is the first complete and formal presentation of the language and its semantics. It also presents uses cases of ABCD for the modelling and analysis of various systems.