摘要：随着计算机技术应用的日益广泛,目前在航天、通信、交通等系统上采用嵌入式软件实现的功能越来越多,并且成为系统的独立产品和独立构件,发挥着至关重要的作用。而嵌入式软件的硬实时性的特点也要求必须对软件的需求进行验证,尤其是实时性的验证。因此,项目在设计和编码前进行需求验证不仅必要,而且必不可少。本文结合模型驱动开发方法,将需求验证与模型验证结合提出了一种嵌入式软件的形式化验证方法。