变换模型是基于形式化规格说明语言及程序变换的软件开发模型。它采用形式化的软件开发方法，对形式化的软件规格说明进行一系列自动或半自动的程序变换。最后映射成计算机系统能够接受的程序系统。采用变换模型的软件过程如概述图所示。为了确认形式化规格说明与软件需求的一致性，往往以形式化规格说明为基础开发一个软件模型。用户可以从人机界面、系统主要功能、性能等几个方面对原型进行评审。必要时，可以对软件需求、形式化规格说明和原型进行修改，直至原型被确认时为止。这时软件开发人员就可以对形式化的规格说明进行一系列的程序变换，直至生成计算机系统可以接受的目标代码。