Coloured Petri Nets: Modelling and Validation of Concurrent Systems (2009) [pdf]

Such a coincidence! I have actually created a Petri net implementation for Common Lisp two months ago to model an asynchronous process of downloading various dependend things from a REST web server. The tokens may be arbitrary Lisp data and transitions are functions with some internal structure (Lispspeak: funcallable instances). The net functions well with multiple threads and is therefore fully async.

https://github.com/phoe/petri

If you want to try modelling some stuff with petri nets, or rather more advanced abstractions, there's the FLOSS tool called "Renew" (Reference Net Workshop) from the university of Hamburg. The UX could be better but it's an interesting tool. It uses reference nets (which are more powerful than petri nets because you can have subnets and modularize your simulations quite nicely). It's in Java and you can execute Java-code from the models (if a transaction fires) which is pretty interesting. The last update to the site was in 2016 but the tool is stable and can be used. They also have a nice User Guide as PDF on the site:

http://www.renew.de/

This thread a few days ago also mentions Petri Nets: https://news.ycombinator.com/item?id=19025639

Petit nets in general are a great tool for managing concurrency. My university’s concurrent programming course used a fairly limited tool called LTSA to model concurrent systems, and that was a great little tool for designing and reasoning about concurrent systems.

Biggest limitation was the lack of code gen - it can prove things about a concurrent system (completion, deadlock feee, global operation ordering etc) but that was only accurate if the coded implementation had identical semantics.

Embarrassing story:

I did my dissertation research on formal methods and network protocols. Somehow, I managed to completely ignore Petri nets.

Then I had an interview with Boeing, where they apparently used nothing else.

I think I managed to convince them I didn't understand my own research. Worst interview I ever had.

This ”cpn tools” the book is about is cool for a number of reasons but I will start with two: it’s written in the Beta languange and it has its own ml dialect called cpn ml. I look forward to diving in deeper!