Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model checking strategy-controlled systems in rewriting logic

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

TL;DR

This paper discusses model checking for strategy-controlled systems, and presents a strategy-aware extension of the Maude LTL model checker, and discusses the expressivity of the strategy language in relation to model checking.

Abstract

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.

Model checking strategy-controlled systems in rewriting logic

TL;DR

This paper discusses model checking for strategy-controlled systems, and presents a strategy-aware extension of the Maude LTL model checker, and discusses the expressivity of the strategy language in relation to model checking.

Abstract

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.
Paper Structure (32 sections, 15 theorems, 20 equations, 3 figures, 2 tables)

This paper contains 32 sections, 15 theorems, 20 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Languages and automata over finite and infinite words
  4. Strategies
  5. Strategies
  6. Model checking
  7. The syntax and semantics of LTL
  8. The automata-theoretic approach for LTL model checking
  9. Rewriting logic and Maude
  10. Model checking abstract strategy-controlled systems
  11. The Maude strategy language and its semantics
  12. Strategy modules
  13. Model checking for the Maude strategy language
  14. Expressiveness of the language and decidability
  15. The Maude strategy-aware model checker
  16. ...and 17 more sections

Key Result

proposition \@thmcounterproposition

Given $E \subseteq S^\omega$, there is a finite Kripke structure $\mathcal{K}'$ such that $\ell(\Gamma^\omega_{\mathcal{K}'}) = \ell(E)$ iff $\ell(E)$ is closed and $\omega$-regular.

Figures (3)

  • Figure 1: Solution and deadlock states in $\mathcal{O}^{\alpha, t}$ and their adjustments.
  • Figure 2: Structure of the strategy model checker modules.
  • Figure 3: Example hierarchy of tasks (boxes) and processes (circles) with a task info.

Theorems & Definitions (28)

  • definition \@thmcounterdefinition
  • definition \@thmcounterdefinition
  • proposition \@thmcounterproposition
  • definition \@thmcounterdefinition
  • proposition \@thmcounterproposition
  • corollary \@thmcountercorollary
  • proposition \@thmcounterproposition
  • proposition \@thmcounterproposition
  • proposition \@thmcounterproposition
  • definition \@thmcounterdefinition
  • ...and 18 more