一种面向核心交易系统架构代码实现的抽象建模及验证方法

本发明是一种面向核心交易系统架构代码实现的抽象建模及验证方法，包括：A对交易系统的架构进行建模与验证：通过从架构框架的代码实现与开发设计文档中抽取相关信息，使用抽象建模技术构建已有系统的行为模型，利用UML顺序图建模系统的进程通信过程，将UML顺序图转换成CSP的形式化模型，并使用PAT验证器进行安全性质的验证分析；B对交易系统中集群选主模块进行建模及验证：构建集群选主过程中各个节点的状态机模型，构建系统动态模型，并使用PAT验证器对选主过程的正确性进行验证分析。本发明优点在于：解决交易系统架构中各进程间通信过程及集群选主过程中各个节点的状态变迁建模问题，提升建模及安全性验证分析能力。