When Concurrent Control Meets Functional Requirements, or Z + Petri-Nets. - Frédéric Peschanski; David Julien 002 (ZB, 2003)