Formalisation of a production system modelling language the operational semantics of X Core

The formal language X Core is derived from the systems engineering specification language X. The language has its roots in Mechanical Engineering where it was designed to specify and analyse production systems. These production systems are described by concurrent communicating processes and can be analysed with the X simulator. X Core is a formalisation and simplification of the semantics of the X language. Our motivation to design X Core is the lack of a properly defined semantics of the X specification language itself and the need for improved opportunities for the analysis of production systems. The operational semantics of X Core is defined in a standard SOS-style. A bisimulation on X Core processes is defined and shown to be a congruence. Based on this bisimulation, properties and time aspects of X Core processes are discussed. The relation between X and X Core is explained by means of a translation scheme. Finally, an example specification of a production system is given and conclusions are drawn.