模型检测是一种检测有限状态并发系统的自动化检测技术。它是检测系统模型是否满足系统规约。模型检测在硬件和通讯协议的分析与验证中已经取得了很大的成功，如何将这一技术应用于软件，是具有挑战性的课题。由于软件涉及无穷数据域上的运算而往往呈现出无穷状态，这是软件模型检测的主要难点。但是很多系统(如控制软件)并不涉及复杂的数值计算，往往只用到线性实数约束或整数加减等简单的运算，因此可以采用诸如线性约束求解等技术实现模型检测，即使是一般的商用软件，也可以通过应用抽象等技术映射到有限域上进行模型检测。 本文以商用IC卡消费系统为背景，研究模型验证应用于软件系统的关键技术。主要研究成果包括： (1)提出了一种基于抽象技术的IC卡消费系统的建模方法，该方法能有效地建立基于UML用例图的形式化软件模型。 (2)提出了基于时态逻辑的软件规约描述方法，用于表达商业软件系统数据同步、无死锁等关键性质。 (3)将模型验证技术应用于商用卡消费系统的验证和分析，并利用验证工具XSPIN实现了自动验证。