The purpose of this lecture is to provide an overview of the application of a High-Level Petri Net-based formal methodology that covers the development-life-cycle from requirements-analysis through to design-validation and implementation of flexible production systems and their supervisory control system in an integrated manner. Formal models of both systems are systematically and progressively built and set into operation, based on High-Level Petri net (H-L-PN) theory, preserving the desired specifications of flexible production system and supervisory controller all along the design-implementation process.