目前,在机器人控制领域,面向服务的控制系统可提高控制系统的重用性和可扩展性,将形式化建模和模型验证技术应用于面向服务的机器人控制系统,可以提高系统的开发效率,同时保证系统的性能需求。形式化建模主要用于保证系统原型设计和具体实现的一致性,使得对原型设计进行修改能够自动地反映到具体的代码实现中,保持前后的统一,并减少重复的工作量。而模型验证主要用于对原型设计进行仿真验证,保证系统的合理性和可用性。本文研究了模型驱动架构的形式化建模方法以及仿真验证中的模型验证技术在机器人控制系统中的具体应用。采用形式化建模方法对机器人控制系统进行描述,并设计和构建了控制系统的建模环境;采用基于时间自动机的模型验证技术,设计了机器人控制系统的仿真验证模型;同时,设计基于统计学的验证模型,有效地解决模型验证过程中存在的状态爆炸问题;提出组件化的代码生成技术,能够实现模型之间的自动转换,并自动生成面向服务的机器人控制系统代码。最后,对面向服务的机器人控制系统模型进行仿真验证实验,保证组件化自动生成代码的合理性和可用性,并通过代码对比实验验证了组件化自动生成的代码的优势。