Automatic synthesis system for resource controllers in concurrent euclid

Abstract

Since resource controllers that control accesses to shared resources play an indispensable role in the functioning of concurrent systems, it is highly desirable to develop a mechanism to produce reliable resource controllers. In this thesis, a design of an automatic synthesis system is proposed to develop reliable resource controllers. Input to the system is specifications of the shared resource, operations on the resources and the synchronization requirements. These specifications are translated into Concurrent Euclid which is a monitor type concurrent programming language. The meaning-preserving transformation rules are used for systematically synthesizing codes of a resource controller from the given specifications.