Abstract: Business rules are statements constraining business actions. they are context dependent, and may remain unchanged over a long period of time. The dynamic applictionof business rules to business actions requires a clear separation of the actions from the rules so that changes to business rules can be done without affecting 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 specification language to write business rules. This language, called Business Transaction Object-Z (BTOZ), is a conservative extension of the Object-Z specification language. The paper also illustrates through a case study how BTOZ can be used to develop a business model.