Rewriting Modulo SMT and Open System Analysis

Rocha, Camilo; Meseguer, José; Cesar Munoz

Permalink

https://hdl.handle.net/2142/91638 Copy

Description

Title

Rewriting Modulo SMT and Open System Analysis

Author(s)

• Rocha, Camilo
• Meseguer, José
• Cesar Munoz

Issue Date

2016-10-02

Keyword(s)

• rewriting
• satisfaction modulo theories
• reachability analysis
• open systems
• Maude

Abstract

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/91638

Sponsor(s)/Grant Number(s)

NSF Grant CNS 13-19109 and NASA Research Cooperative Agreement No. NNL09AA00A

Owning Collections