Formal Verification of Ecosystem Restoration Requirements using UML and Alloy

TL;DR

The paper addresses the need for rigor in software supporting ecosystem restoration by combining a UML-based metamodel with Alloy formalization to verify restoration requirements. It develops a semi-formal metamodel for ecosystems and their restoration goals, translates it into Alloy, and demonstrates safety and liveness verification on the CRESTO Costa Rica case study. The key contributions include a concrete UML-to-Alloy translation, a formal Alloy core for ecosystem concepts, and an instantiation (CRESTO) with verified properties that highlight both validated and counterexample scenarios. The work advances formal software engineering for environmental applications and suggests a path toward AI-enabled and remote sensing tools built on verified restoration requirements.

Abstract

United Nations have declared the current decade (2021-2030) as the "UN Decade on Ecosystem Restoration" to join R\&D forces to fight against the ongoing environmental crisis. Given the ongoing degradation of earth ecosystems and the related crucial services that they offer to the human society, ecosystem restoration has become a major society-critical issue. It is required to develop rigorously software applications managing ecosystem restoration. Reliable models of ecosystems and restoration goals are necessary. This paper proposes a rigorous approach for ecosystem requirements modeling using formal methods from a model-driven software engineering point of view. The authors describe the main concepts at stake with a metamodel in UML and introduce a formalization of this metamodel in Alloy. The formal model is executed with Alloy Analyzer, and safety and liveness properties are checked against it. This approach helps ensuring that ecosystem specifications are reliable and that the specified ecosystem meets the desired restoration goals, seen in our approach as liveness and safety properties. The concepts and activities of the approach are illustrated with CRESTO, a real-world running example of a restored Costa Rican ecosystem.

Figures (3)

• Figure 1: Metamodel for Ecosystem Requirements Specification
• Figure 2: Alloy Analyzer output for the "RestorationShallOccurOnEcosystem" safety property and "EverySpeciesHasHabitat" liveness property. The output reveals that no counterexamples are found for both properties, indicating that the assertion may be valid within our formal model.
• Figure 3: Alloy Analyzer output presenting a counterexample for the "speciesInRestorationGoal" safety property check. The counterexample demonstrates that species may not be present in an ecosystem with a restoration goal associated with it, which invalidates the defined safety property in our formal model.

Theorems & Definitions (4)

• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition