TY - JOUR
T1 - Rewriting modulo SMT and open system analysis
AU - Rocha, Camilo
AU - Meseguer, José
AU - Muñoz, César
N1 - The authors would like to thank S. Eker for fruitful discussions on these ideas and their implementation in Maude, and the anonymous referees for their very helpful comments that helped us improve the paper. This work was partially supported by NSF Grant CNS 13-19109 . The first author would like to thank the National Institute of Aerospace for a short visit supported by the Assurance of Flight Critical System's project of NASA's Aviation Safety Program at Langley Research Center under Research Cooperative Agreement No. NNL09AA00A .
PY - 2014
Y1 - 2014
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 infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, 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 a real-time system that is beyond the scope of timed-automata methods.
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 infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, 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 a real-time system that is beyond the scope of timed-automata methods.
UR - https://www.scopus.com/pages/publications/84911972119
UR - https://www.scopus.com/pages/publications/84911972119#tab=citedBy
U2 - 10.1007/978-3-319-12904-4_14
DO - 10.1007/978-3-319-12904-4_14
M3 - Article
AN - SCOPUS:84911972119
SN - 0302-9743
VL - 8663
SP - 247
EP - 262
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -