使用UML和Alloy对生态系统恢复需求的形式化验证
软件工程
2024-06-11 v1
摘要
联合国已宣布当前十年（2021-2030）为“联合国生态系统恢复十年”，以联合研发力量应对持续的环境危机。鉴于地球生态系统及其为人类社会提供的相关关键服务的持续退化，生态系统恢复已成为一个重大的社会关键问题。需要严格开发管理生态系统恢复的软件应用。可靠的生态系统和恢复目标模型是必要的。本文提出了一种从模型驱动软件工程角度使用形式化方法进行生态系统需求建模的严格方法。作者用UML元模型描述了所涉及的主要概念，并在Alloy中引入了该元模型的形式化。形式化模型通过Alloy Analyzer执行，并检查安全性和活性属性。该方法有助于确保生态系统规范是可靠的，并且指定的生态系统满足期望的恢复目标，在我们的方法中视为活性和安全性属性。该方法和活动的概念通过CRESTO（一个真实的哥斯达黎加恢复生态系统运行示例）进行说明。
引用
@article{arxiv.2405.20722,
title = {Formal Verification of Ecosystem Restoration Requirements using UML and Alloy},
author = {Tiago Sousa and Benoît Ries and Nicolas Guelfi},
journal= {arXiv preprint arXiv:2405.20722},
year = {2024}
}