AWS云运维自动化中的程序生成方法研究

在AWS云运维团队的应用科学实习期间，研究者探索了程序生成方法以简化DevOps工程师的工作流程。DevOps工程师负责在云平台上配置、运营和管理应用程序，包括部署升级、监控安全性和确保云资源始终处于最佳运行状态。他们的日常工作可能涉及重复性任务，尤其是当AWS应用程序涉及数百甚至上万台机器时。

约束编程实现重复任务自动化

研究者采用创新方法简化AWS系统管理，将程序合成与约束编程相结合来自动化常见任务。这种方法能够保证预期结果或目标的实现。

“程序合成是从期望行为的描述中自动生成编程语言计算机程序的任务，无需程序员手动编码，“研究者解释。“它旨在通过弥合人类可读问题描述与实现解决方案的实际计算机代码之间的差距，将计算能力带给更广泛的受众。对于熟练的程序员也很有用，可以自动化实现重复性、无趣的代码片段。”

通过将手动任务的日志文件作为约束条件，研究者使用程序合成创建了"自动化运行手册”——一种可以创建程序来自动化云管理任务并保证准确性的脚本。

“程序合成以数学证明的形式提供正式保证，逐步展示所创建的程序正在执行您要求的操作，“研究者表示。这种方法为需要确保云系统最佳运行的管理者增加了必要的信心水平。

该方法的核心价值在于客户可以直接使用自动化运行手册，无需反复检查。通过约束编程，运行手册保证提供答案，且该答案必须满足所有约束条件。

云运维团队致力于让计算机学会自我编程，使客户能够在不编程的情况下使用云产品。这项研究展示了如何将形式化方法、理论保证和证明用于改进和优化网络，使其更加高效。

研究者来自卡内基梅隆大学，专注于自动推理和程序合成领域。在实习期间，她发现某中心的研究过程与学术界相似，更多由问题陈述、假设和普遍好奇心驱动。

科学实习生被鼓励进行可发表的研究，这与软件工程实习形成鲜明对比。这种纯研究具有明显的实际影响，特别是考虑到每天有数百万人使用云服务平台。

该研究不仅展示了程序合成在云运维自动化中的实际应用，也为来自小国的研究人员在国际舞台上产生重大影响树立了榜样。