面向对象程序设计技术是软件开发历史上最重要的贡献之一,它通过封装、继承以及多态等机制良好的实现了抽象、信息隐藏与模块化,使得开发人员有效的开发并控制大型复杂的系统成为可能。然而它只能较好的解决关注点的纵向泛化方面的关系,横向依赖关系往往被忽略,结果导致软件系统实现过程中,一些横切的关注点离散的分布于各个模块中,一些逻辑业务代码和横向上的关注点难于清晰的定位和代码的“缠结”现象,缠结现象是导致现有软件系统不必要的复杂性的核心。它降低了系统的内聚度以及可理解性,增加了程序设计出错的机会,使得一些功能构件难以复用,项目难于继续开发和维护。面向方面的程序设计技术很好继承了面向对象的程序设计技术的优点,并能弥补了它在程序设计时对横向关注点处理的不足。它能深入到对象内部,将横切关注点抽取出来并进行模块化,使得很好的实现了与系统核心关注点相分离。从而有效的降低了系统模块间的耦合度,将面向方面的程序设计思想应用到实时系统的分析与设计阶段,能大大增强对系统的理解性,提高代码的可重用性和降低系统模块之间的耦合度。随着软件的广泛应用,特别是软件在尖端领域的应用,软件安全性和可靠性成为一个非常重要的问题。形式化方法以数学为基础来定义硬件系统和软件系统的规约并对系统进行验证。其核心在于构造数学模型以及通过计算的方式对模型性质进行分析和验证。它能提供一致性、完整性、规约、实现和精准性等概念的精确定义,能够清晰、精确、抽象、简明地规范和验证软件系统及其性质,从而能极大地提高软件的安全性和可靠性。本文采用形式化方法来对CPS系统进行建模,结合AOP技术将CPS抽象分离出信息、通信和物理三个方面,采用ZimOO对系统的信息方面进行建模,用CSP对系统的通信方面进行建模,用微分动态逻辑对系统的物理方面进行建模,待建立好这三个子方面模型后,再通过面向方面的织入思想,将该三个子方面织入到主系统中,形成一个完整的系统模型。文章最后通过一个列车调度控制系统实例对这种形式化建模过程进行说明和验证。