随着软件系统的结构越来越复杂,规模越来越庞大,复杂程度越来越高,软件出现错误的可能性及其造成的危害也日益突出。并发系统在以其并发性而极大地提高系统性能的同时,也因其各线程或进程交互协作,极大的增加了设计的复杂性和系统运行期间的出错的可能性。在并发系统的设计中,主要存在三个方面的问题。第一个问题涉及到并发系统的表示问题。传统的并发系统设计方法,在实际开发中也起到了很好的指导性作用。但是,这些表示并发系统的方法不能给开发者一个简单而直观的方式去从宏观上看待整个系统。第二个问题和达到系统性能要求相关。在传统的设计领域,主要依靠系统化的测试方法去确定是否设计的目标系统最终达到了预期的要求。在设计的过程中,很多潜藏的错误不易被发现,例如死锁。第三个问题涉及到代码生成。尽管熟练的程序员能够编写出技巧性极高的高效代码。但是人总是会出现错误,特别是在一些对控制逻辑要求极为严格的代码段中,犯错误是很正常也很常见的情况。形式化方法的出现在一定程度上成为了解决上述问题的重大进步,其因采用基于代数、集合论等数学理论作为基础,使得系统设计具有了严密性和准确性的特点。采用形式化方法对系统进行设计、验证,不仅提供了开发者一种直观地看待系统的方式,也使得开发者能够在设计阶段就准确把握目标系统的各项性能,并在开发阶段中以这些准确的形式化规范指导开发者的开发工作。基于形式化的自动代码生成则不仅节约了开发者的开发工作,而且提供了准确的控制逻辑,使得开发者可以将注意力集中到功能实现代码的编写上去。