郭华 / Hua Guo

计算机软件与理论博士，现为华东师范大学博士后。主要研究方向包括云原生数据库、分布式系统、形式化方法在系统软件中的应用、云环境零信任安全以及 AI 辅助软件工程。曾参与列存储数据库、大数据分析平台、地图基础数据平台等工程系统研发，当前重点开展新型数据库管理与应用执行一体化系统研究。

教育经历

• 中国人民大学，计算机软件与理论，博士，2019.9 – 2024.12
• 中国人民大学，计算机软件与理论，硕士，2016.9 – 2019.6
• 海南大学，计算机科学与技术，学士，2007.9 – 2011.6

工作经历

华东师范大学，博士后研究人员

2024.3 – 至今

围绕云原生数据库、数据密集型应用执行、系统软件验证与 AI 辅助软件工程等方向开展研究工作，重点关注数据库系统架构、分布式事务处理、形式化验证方法与系统工程实践的结合。

开珀卡珀（scuptio），创始人

2023.1 – 至今

负责MuduDB数据库系统、系统软件质量保障相关项目的设计与研发，主要项目包括：

• MuduDB：面向数据密集型应用的新型数据库系统，目标是让应用逻辑能够直接运行和部署在数据库之上。
• sedeve-kit：形式化验证与测试工具，面向数据库系统的规范建模、测试生成与行为验证。
• 零信任系统：面向云环境与分布式系统的零信任安全机制研究与原型开发。

百度地图

2014.7 – 2015.7

参与百度地图基础数据平台相关研发工作，主要涉及地图基础数据处理、平台化支撑与数据服务能力建设。

东方国信

2012.5 – 2014.7

参与列存储数据库系统与大数据分析系统研发，主要关注数据存储、查询处理与分析型系统工程实现。

目标在线

2011.8 – 2012.5

从事游戏开发相关工作，参与在线游戏系统的功能开发与工程实现。

研究方向

• 云原生数据库系统：数据库系统架构、事务处理、数据密集型应用执行、云环境数据库基础设施。
• 分布式系统：共识协议、容错机制、分布式事务、系统一致性与可靠性。
• 形式化方法与系统软件验证：TLA+ 规范建模、规范驱动开发、数据库与分布式系统正确性验证。
• 云上零信任安全：云环境访问控制、身份认证、最小权限与系统安全边界设计。
• AI 辅助软件工程：大模型辅助需求分析、规范生成、代码生成、测试生成与工程流程自动化。

代表性论文与会议

学术论文

1. Hua Guo, Yunhong Ji, Huiqi Hu, Xuan Zhou. A Composable Architecture for Cloud Transactional DBMS. APWeb/WAIM (3), 2024: 428–443.

2. Hua Guo, Yunhong Ji, Xuan Zhou. The Development of a TLA+ Verified Correctness Raft Consensus Protocol. APWeb/WAIM (5), 2024: 459–469.

3. Hua Guo, Xuan Zhou, Le Cai. Lock Violation for Fault-tolerant Distributed Database System. ICDE, 2021: 1416–1427. 相关方法已在 Microsoft Orleans 中实现。

技术报告与会议报告

1. 郭华. 使用 TLA+ 形式化规范驱动开发保证数据库系统软件质量. 中国数据库技术大会（DTCC 2024）.

2. Hua Guo. Specification-Driven Development With TLA+. TLA+ Conference 2024.

代表项目

MuduDB：数据库管理与应用执行一体化系统

MuduDB 是面向数据密集型应用的新型数据库系统，旨在将数据管理、事务处理、状态维护、应用执行与部署分发整合到统一平台中，使应用逻辑能够更靠近数据运行，减少传统应用层与数据库层之间的反复通信开销。

项目重点关注：

• 数据库内应用执行模型；
• 事务处理与应用逻辑的统一调度；
• 面向云环境的数据局部性与分区执行；
• 数据库系统正确性验证与测试；
• 面向新型数据密集型应用的系统架构设计。

sedeve-kit：形式化驱动开发工具

sedeve-kit 面向数据库与分布式系统的正确性保障问题，支持通过形式化规范、测试生成和系统行为检查等方式，提高复杂系统在并发、故障和边界条件下的可靠性。

关键词

数据库系统 / 云原生数据库 / 分布式系统 / 形式化方法 / TLA+ / 系统软件验证 / 零信任安全 / AI 辅助软件工程