TY - GEN
T1 - Symbolic execution and reachability analysis using rewriting modulo SMT for spatial concurrent constraint systems with extrusion
AU - Romero, Miguel
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2018, Springer International Publishing AG, part of Springer Nature.
PY - 2018
Y1 - 2018
N2 - The usual high degree of assurance in safety-critical systems is being challenged by a new incarnation of distributed systems exposed to the presence of hierarchical computation (e.g., virtualization resources such as container and virtual machine technology). This paper addresses the issue of symbolically specifying and verifying properties of distributed hierarchical systems using rewriting modulo SMT, a symbolic approach for rewriting logic that seamlessly combines rewriting modulo theories, SMT solving, and model checking. It presents a rewrite theory R implementing a symbolic executable semantics of an algebraic model of spatially constrained concurrent process with extrusion. The underlying constraint system in R is materialized with the help of SMT-solving technology, where the constraints are quantifier-free formulas interpreted over the Booleans and integers, and information entailment is queried via semantic inference. Symbolic rewrite steps with → R capture all possible traces from ground instances of the source state to the ground instances of the target state. This approach, as illustrated with some examples in the paper, is well-suited for specifying and proving (or disproving) existential reachability properties of distributed hierarchical systems, such as fault-tolerance, consistency, and privacy.
AB - The usual high degree of assurance in safety-critical systems is being challenged by a new incarnation of distributed systems exposed to the presence of hierarchical computation (e.g., virtualization resources such as container and virtual machine technology). This paper addresses the issue of symbolically specifying and verifying properties of distributed hierarchical systems using rewriting modulo SMT, a symbolic approach for rewriting logic that seamlessly combines rewriting modulo theories, SMT solving, and model checking. It presents a rewrite theory R implementing a symbolic executable semantics of an algebraic model of spatially constrained concurrent process with extrusion. The underlying constraint system in R is materialized with the help of SMT-solving technology, where the constraints are quantifier-free formulas interpreted over the Booleans and integers, and information entailment is queried via semantic inference. Symbolic rewrite steps with → R capture all possible traces from ground instances of the source state to the ground instances of the target state. This approach, as illustrated with some examples in the paper, is well-suited for specifying and proving (or disproving) existential reachability properties of distributed hierarchical systems, such as fault-tolerance, consistency, and privacy.
UR - http://www.scopus.com/inward/record.url?scp=85045305229&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-77935-5_29
DO - 10.1007/978-3-319-77935-5_29
M3 - Conference contribution
AN - SCOPUS:85045305229
SN - 9783319779348
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 435
EP - 451
BT - NASA Formal Methods 10th International Symposium, 10th International Symposium, NFM 2018 Newport News, Proceedings
A2 - Dutle, Aaron
A2 - Munoz, Cesar
A2 - Narkawicz, Anthony
PB - Springer Verlag
T2 - 10th International Symposium on NASA Formal Methods, NFM 2018
Y2 - 17 April 2018 through 19 April 2018
ER -