TY - JOUR
T1 - Rewriting modulo SMT and open system analysis
AU - Rocha, Camilo
AU - Meseguer, José
AU - Muñoz, César
N1 - Publisher Copyright:
© 2016 Elsevier Inc.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85005963591&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-12904-4_14
DO - 10.1007/978-3-319-12904-4_14
M3 - Article
AN - SCOPUS:84911972119
SN - 2352-2208
VL - 86
SP - 269
EP - 297
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
IS - 1
ER -