Abstract: Increasing complexity in engineering projects together with requirements on reduced design time and low costs raise difficult challenges in industry. Thus, effective tools for correct by construction design of for design verification are very much needed. In practice, design and verification are done hierarchically , at several levels of abstraction. This book addresses the design of tools for correct by construction synthesis at the discrete-event level of abstraction. The approach of this book is to use Petri nets as discrete-event models and structural methods for the synthesis of supervisors enforcing the design specifications. This approach promises significant computational benefits.