Business modelling methods are popular but, since they operate primarily in the early stages of software lifecycles, most are informal. This talk presents how we have used a conventional formal notation (first order predicate logic) in combination with automated support tools to replicate the key components of an established, informal, business modelling method: IBM's Business System Development Method (BSDM).
We describe the knowledge which we represent formally at each stage in the method and explain how the move from informal to formal representation allows us to provide guidance and consistency checking during the lifecycle of the model development. It also allows us to extend the original method to a model execution phase which is not described in the original informal method; the details of the execution phase will not be present in the talk due to time limitation but is given in the reference paper. A reference paper is available at: http://www.dai.ed.ac.uk/groups/ssp/psfiles/jessica/jes2.ps.