Rewriting modulo SMT and open system analysis

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. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. 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.

• Autores: Rocha, Camilo; Meseguer, José; Muñoz, César
• Tipo de recurso: Article of journal
• Fecha de publicación: 2016
• Institución: Escuela Colombiana de Ingeniería Julio Garavito
• Repositorio: Repositorio Institucional ECI
• Idioma: eng
• OAI Identifier: oai:repositorio.escuelaing.edu.co:001/1866
• Acceso en línea: https://repositorio.escuelaing.edu.co/handle/001/1866
• Palabra clave: Relaciones de conjuntos sincrónicos; Semántica síncrona; Reescritura de lógica; Simulación formal y verificación; Synchronous set relations; Synchronous semantics; Rewriting logic; Formal simulation and verification; PLEXIL
• Rights: openAccess
• License: © 2016 Elsevier Inc. All rights reserved.