A formal specification approach for holonic control systems: the ADACOR case

Distributed manufacturing control systems, such as Holonic Control Systems (HCSs), are difficult to apprehend and to design, due to the presence of many autonomous, concurrent and asynchronous activities. A formal specification methodology allowing to understand, to synthesise the system specifications and to validate the correctness of their models would play a key role in its design and later in its implementation. This paper presents an approach to the formal specification of HCSs based on high-level Petri nets. The proposed approach is tested in the specification of the ADACOR HCS.