This work aims to provide a general mechanism for safety enforcement in rewriting logic computations. Our technique relies on an assertion-guided model transformation that leverages the newly defined Maude strategy language for ensuring rich safety policies in non-deterministic programs. The transformed system is guaranteed to comply with user-defined invariants that are expressed in a strategy-based, pattern-matching logic, thus preventing the concurrent system to reach any unsafe states. The performance and scalability of the technique is empirically evaluated and benchmarked on a set of realistic programs.
Safety enforcement via programmable strategies in Maude
Ballis D.;
2023-01-01
Abstract
This work aims to provide a general mechanism for safety enforcement in rewriting logic computations. Our technique relies on an assertion-guided model transformation that leverages the newly defined Maude strategy language for ensuring rich safety policies in non-deterministic programs. The transformed system is guaranteed to comply with user-defined invariants that are expressed in a strategy-based, pattern-matching logic, thus preventing the concurrent system to reach any unsafe states. The performance and scalability of the technique is empirically evaluated and benchmarked on a set of realistic programs.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
