Model checking strategy-controlled systems in rewriting logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913196959334400 |
|---|---|
| author | Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto |
| author_facet | Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto |
| contents | Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive.
In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_07616 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Model checking strategy-controlled systems in rewriting logic Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto Logic in Computer Science 68Q60 F.4.1; F.3.1 Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive. In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared. |
| title | Model checking strategy-controlled systems in rewriting logic |
| topic | Logic in Computer Science 68Q60 F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2401.07616 |