Business rules are statements constraining business actions. Every business activity that involves a sequence of business actions should be conducted by applying business rules governing each action in the sequence. Business rules are context dependent, and may remain unchanged over a long period of time. The dynamic application of business rules to business actions requires a clear separation of business actions from business rules so that changes to business rules can be done without a ecting the actions on which they are applied. In addition, rules can also be applied to a family of implementations of a business action. This paper introduces a formal theoretical business model and a speci cation language to write business rules. This language, called Business Transaction Object-Z (BTOZ), is a conservative extension of the Object-Z speci cation language. The paper also illustrates through a case study how BTOZ can be used to develop a business model.'