Rewriting modulo SMT and open system analysis

详细信息    查看全文

• 作者：Camilo Rocha^a ; ^{camilo.rocha@javerianacali.edu.co} ; José ; Meseguer^b ; ^{meseguer@cs.illinois.edu} ; Cé ; sar Muñ ; oz^c ; ^{cesar.a.munoz@nasa.gov}
• 刊名：Journal of Logical and Algebraic Methods in Programming
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：86
• 期：1
• 页码：269-297
• 全文大小：807 K
• 卷排序：86

文摘

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.