Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum – no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as an advanced discipline for later study. Formal verification of system properties remains considered an advanced and difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. Our experience, from over 30 years of teaching concurrency and formal methods, is that when both are presented together, there is a happy symbiosis providing strong mutual support that transforms both disciplines from advanced and hard to basic and simple. Of course, the model of concurrency and formal methods presented must be simple, powerful and consistent with each other … and, of course, we are talking about process orientation and process algebra.

As with many other disciplines, it is important to use a well-defined methodology that shows how aspects of the disciplines relate to each other and how work flows between them. We introduce a workflow methodology for the mutual development and verification of concurrent systems that serves as a good foundation for students and novices – as well as mature software engineers – learning to integrate formal verification into their development cycle. Such a workflow methodology should be a fundamental element of any future software engineer's tool kit – to be used, together with established software engineering techniques, every day as a matter of course. Concurrency and verification can and should live in symbiosis. By following a well-defined workflow that makes this explicit, major benefits (such as faster development, right-first-time and easier maintenance) can be realised.

This talk will present an approach developed over many years at Kent and UNLV for teaching concurrency with verification and share some of our materials and experiences.