Concurrent program synthesis based on supervisory control

The paper introduces a new area of application of the supervisory control (SC) methods and a project dealing with this research topic. Based on the observation that various constraints on the operation and synchronization of concurrent processes can be expressed in terms of SC specifications, the paper proposes the application of SC to the automation of concurrent program synthesis. Specifically, the paper proposes a three-stage approach allowing to generate automatically the part of the programs that deals with the coordination of concurrent processes. In a first stage, Petri net models are extracted from a high level specification. An SC specification is also extracted. Then, SC is applied to generate the supervisor enforcing the specification. Finally, the programs representing the processes and the supervisor are generated. This work is motivated by the difficulty of writing correctly concurrent programs. Since this difficulty is due to the constraints on the operation and synchronization of concurrent processes, research in this area has the potential of simplifying the development of concurrent programs.