Other (Reports)
Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
Sousa, Tiago; Ries, Benoit; Guelfi, Nicolas
2023
 

Files


Full Text
2023-04-21 ASOFT 2023 submitted version.pdf
Author preprint (1.83 MB)
Request a copy

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Language and Formal Methods; Formal Software Engineering; Requirements Engineering; Ecosystem Restoration Modeling; Alloy; UML
Abstract :
[en] 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.
Disciplines :
Computer science
Author, co-author :
Sousa, Tiago  ;  University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Ries, Benoit ;  University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Guelfi, Nicolas ;  University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Language :
English
Title :
Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
Publication date :
2023
Report number :
TR-LASSY-23-02
Number of pages :
20
Available on ORBilu :
since 02 May 2023

Statistics


Number of views
86 (32 by Unilu)
Number of downloads
3 (2 by Unilu)

Bibliography


Similar publications



Contact ORBilu