In this paper we consider a formalism for studying specifications of the structure and behaviour of enterprises. An enterprise is an organisational system producing goods or services for the market in order to make financial profit. An important issue is the value cycle, used for determining the entrepreneurial viability. The formalism offers the advantage of rigorous automatic analysis in design time of central properties of the enterprise specification. The formalism uses so-called value cycle nets, based on Petri nets.