Publication:
Rewriting modulo SMT and open system analysis

Thumbnail Image
Files

Files

Rewriting modulo SMT and open system analysis.pdf (807.86 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Meseguer, José
Muñoz, César
Abstract (Spanish)
Este artículo propone la reescritura de módulo SMT, una nueva técnica que combina el poder de la resolución SMT, la reescritura de teorías de módulo y la verificación de modelos. La reescritura del módulo SMT es ideal para modelar y analizar las propiedades de accesibilidad de los sistemas abiertos de estado infinito, es decir, los sistemas que interactúan con un entorno no determinista. Dichos sistemas exhiben tanto un no determinismo interno, que es propio del sistema, como un no determinismo externo, que se debe al entorno. En un formalismo reflexivo, como la lógica de reescritura, la reescritura del módulo SMT se puede reducir a la reescritura estándar. Por lo tanto, la reescritura del módulo SMT extiende naturalmente las técnicas de análisis de accesibilidad basadas en la reescritura, que están disponibles para sistemas cerrados, a sistemas abiertos. Además, una sola expresión de estado con restricciones simbólicas ahora puede denotar un conjunto infinito de estados concretos. La técnica propuesta se ilustra con el análisis formal de: (i) un sistema en tiempo real que está más allá del alcance de los métodos de autómatas cronometrados y (ii) detección automática de violaciones de accesibilidad en un lenguaje sincrónico desarrollado para soportar operaciones de naves espaciales autónomas.
Abstract (English)
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.
Extent
29 páginas.
Rights

© 2016 Elsevier Inc. All rights reserved.

URI: https://repositorio.escuelaing.edu.co/handle/001/1866
Collections

Collections

AD - CTG – Informática
References

E. Althaus, E. Kruglov, C. Weidenbach, Superposition modulo linear arithmetic SUP(LA), in: 7th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 5749, Springer, 2009, pp. 84–99.

R. Alur, D.L. Dill, A theory of timed automata, Theor. Comput. Sci. 126 (2) (1994) 183–235.

A. Armando, J. Mantovani, L. Platania, Bounded model checking of software using SMT solvers instead of SAT solvers, Int. J. Softw. Tools Technol. Transf. 11 (1) (2009) 69–83.

A. Arusoaie, D. Lucanu, V. Rusu, A generic framework for symbolic execution, in: 6th International Conference on Software Language Engineering, in: Lect. Notes Comput. Sci., vol. 8225, Springer, 2013, pp. 281–301.

M. Ayala-Rincón, Expressiveness of Conditional Equational Systems with Built-in Predicates, PhD thesis, Universität Kaiserslauten, 1993.

F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.

F. Baader, K. Schulz, Unification in the union of disjoint equational theories: combining decision procedures, J. Symb. Comput. 21 (1996) 211–243.

K. Bae, S. Escobar, J. Meseguer, Abstract logical model checking of infinite-state systems using narrowing, in: 24th International Conference on Rewriting Techniques and Applications, in: Leibniz International Proceedings in Informatics, vol. 21, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 81–96.

K. Bae, C. Rocha, A note on symbolic reachability analysis modulo integer constraints for the CASH algorithm, available at http://maude.cs.uiuc.edu/ cases/scash, 2012.

M.P. Bonacina, C. Lynch, L.M. de Moura, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason. 47 (2) (2011) 161–189.

A. Boudet, Combining unification algorithms, J. Symb. Comput. 16 (6) (1993) 597–626.

A. Bouhoula, F. Jacquemard, Automated induction with constrained tree automata, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 539–554.

A. Bouhoula, F. Jacquemard, Sufficient completeness verification for conditional and constrained TRS, J. Appl. Log. 10 (1) (2012) 127–143, Special issue on Automated Specification and Verification of Web Systems.

R. Bruni, J. Meseguer, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci. 360 (1–3) (2006) 386–414.

M. Caccamo, G.C. Buttazzo, L. Sha, Capacity sharing for overrun control, in: IEEE 34th Real-Time Systems Symposium, IEEE Computer Society, 2000, pp. 295–304.

C. Cadar, D. Dunbar, D.R. Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, in: 8th USENIX Symposium on Operating Systems Design and Implementation, USENIX Association, 2008, pp. 209–224.

C. Cadar, K. Sen, Symbolic execution for software testing: three decades later, Commun. ACM 56 (2) (Feb. 2013) 82–90.

A. Cimatti, A. Griggio, Software model checking via IC3, in: 24th International Conference on Computer Aided Verification, in: Lect. Notes Comput. Sci., vol. 7358, Springer, 2012, pp. 277–293.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C.L. Talcott, All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350, Springer, 2007.

M. Clavel, J. Meseguer, M. Palomino, Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic, Theor. Comput. Sci. 373 (1–2) (2007) 70–91.

G. Delzanno, A. Podelski, Constraint-based deductive model checking, Int. J. Softw. Tools Technol. Transf. 3 (3) (2001) 250–270.

G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A formal analysis framework for PLEXIL, in: 3rd Workshop on Planning and Plan Execution for Real-World Systems, September 2007, pp. 45–51.

[23] G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A Small-Step Semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.

G. Dowek, C.A. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, in: 6th Workshop on Structural Operational Semantics, in: Electron. Proc. Theor. Comput. Sci., vol. 18, 2009, pp. 77–91.

F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving operational termination of membership equational programs, High.-Order Symb. Comput. 21 (1–2) (2008) 59–88.

T. Estlin, A. Jónsson, C. Pas˘ areanu, ˘ R. Simmons, K. Tso, V. Verma, Plan Execution Interchange Language (PLEXIL), Technical Memorandum TM-2006-213483, NASA, 2006.

S. Falke, D. Kapur, Dependency pairs for rewriting with built-in numbers and semantic data structures, in: 19th International Conference on Rewriting Techniques and Applications, in: Lect. Notes Comput. Sci., vol. 5117, Springer, Berlin, Heidelberg, 2008, pp. 94–109.

S. Falke, D. Kapur, Operational termination of conditional rewriting with built-in numbers and semantic data structures, Electron. Notes Theor. Comput. Sci. 237 (2009) 75–90.

S. Falke, D. Kapur, Rewriting induction + linear arithmetic = decision procedure, in: 6th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 7364, Springer, 2012, pp. 241–255.

M. Ganai, A. Gupta, Accelerating high-level bounded model checking, in: 2006 IEEE/ACM International Conference on Computer Aided Design, Nov. 2006, pp. 794–801.

H. Ganzinger, R. Nieuwenhuis, Constraints and theorem proving, in: Constraints in Computational Logics: Theory and Applications, International Sum mer School, in: Lect. Notes Comput. Sci., vol. 2002, Springer, 1999, pp. 159–201.

T. Genet, T. Le Gall, A. Legay, V. Murat, A completion algorithm for lattice tree automata, in: 18th International Conference on Implementation and Application of Automata, in: Lect. Notes Comput. Sci., vol. 7982, Springer, 2013, pp. 134–145.

S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Combination methods for satisfiability and model-checking of infinite-state systems, in: 21st International Conference on Automated Deduction, in: Lect. Notes Comput. Sci., vol. 4603, Springer, 2007, pp. 362–378.

S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Towards SMT model checking of array-based systems, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 67–82.

S. Ghilardi, S. Ranise, MCMT: a model checker modulo theories, in: 5th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 6173, Springer, 2010, pp. 22–29.

J.A. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci. 105 (2) (1992) 217–273.

H. Hojjat, P. Rümmer, P. Subotic, W. Yi, Horn clauses for communicating timed systems, in: N. Bjørner, F. Fioravanti, A. Rybalchenko, V. Senni (Eds.), 1st Workshop on Horn Clauses for Verification and Synthesis, in: Electron. Proc. Theor. Comput. Sci., vol. 169, 2014, pp. 39–52.

H. Kirchner, C. Ringeissen, Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput. 18 (2) (1994) 113–155.

K. Kirchner, H. Kirchner, M. Rusinowitch, Deduction with symbolic constraints, Rev. Intell. Artif. 4 (3) (1990) 9–52.

C. Kop, N. Nishida, Term rewriting with logical constraints, in: 9th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 8152, Springer, 2013, pp. 343–358.

C. Kop, N. Nishida, Automatic constrained rewriting induction towards verifying procedural programs, in: 12th Asian Symposium on Programming Languages and Systems, in: Lect. Notes Comput. Sci., vol. 8858, Springer, 2014, pp. 334–353.

[42] A. Lal, S. Qadeer, S. Lahiri, Corral: A Solver for Reachability Modulo Theories, Technical Report MSR-TR-2012-9, Microsoft Research, January 2012.

K.G. Larsen, P. Pettersson, W. Yi, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf. 1 (1–2) (1997) 134–152.

D. Lucanu, T.-F. Serbanuta, G. Rosu, K framework distilled, in: 9th International Workshop on Rewriting Logic and Its Applications, in: Lect. Notes Comput. Sci., vol. 7571, Springer, 2012, pp. 31–53.

S. Lucas, J. Meseguer, Operational termination of membership equational programs: the order-sorted way, Electron. Notes Theor. Comput. Sci. 238 (3) (2009) 207–225.

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci. 96 (1) (1992) 73–155.

J. Meseguer, Membership algebra as a logical framework for equational specification, in: 12th International Workshop on Recent Trends in Algebraic Development Techniques, in: Lect. Notes Comput. Sci., vol. 1376, Springer, 1997, pp. 18–61.

J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symb. Comput. 20 (1–2) (2007) 123–160.

A. Milicevic, H. Kugler, Model checking using SMT and theory of lists, in: NASA 3rd International Symposium on Formal Methods, in: Lect. Notes Comput. Sci., vol. 6617, Springer, 2011, pp. 282–297.

G. Nelson, D.C. Oppen, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst. 1 (2) (1979) 245–257.

R. Nieuwenhuis, A. Oliveras, C. Tinelli, Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T ), J. ACM 53 (6) (2006) 937–977.

P.C. Ölveczky, M. Caccamo, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, in: L. Baresi, R. Heckel (Eds.), 9th International Conference on Fundamental Approaches to Software Engineering, in: Lect. Notes Comput. Sci., vol. 3922, Springer, 2006, pp. 357–372.

S. Owre, J. Rushby, N. Shankar, PVS: a prototype verification system, in: 11th International Conference on Automated Deduction, in: Lect. Notes Artif. Intell., vol. 607, Springer-Verlag, Saratoga, NY, June 1992, pp. 748–752.

A. Podelski, Model checking as constraint solving, in: 7th International Symposium on Static Analysis, in: Lect. Notes Comput. Sci., vol. 1824, Springer, 2000, pp. 22–37.

C. Rocha, Symbolic Reachability Analysis for Rewrite Theories, PhD thesis, University of Illinois at Urbana-Champaign, 2012.

C. Rocha, H. Cadavid, C.A. Muñoz, R. Siminiceanu, A formal interactive verification environment for the Plan Execution Interchange Language, in: 9th International Conference on Integrated Formal Methods, in: Lect. Notes Comput. Sci., vol. 7321, Springer, 2012, pp. 343–357.

C. Rocha, J. Meseguer, C. Muñoz, Rewriting Modulo SMT, Technical Memorandum NASA/TM-2013-218033, NASA Langley Research Center, Hampton, VA, August 2013.

C. Rocha, J. Meseguer, C. Muñoz, Rewriting modulo SMT and open system analysis, in: 10th International Workshop on Rewriting Logic and Its Appli cations, in: Lect. Notes Comput. Sci., vol. 8663, Springer International Publishing, 2014, pp. 247–262

G. Ro ¸su, A. Stef ¸ anescu, ˘ Matching logic: a new program verification approach, in: 33rd International Conference on Software Engineering, ACM, New York, NY, USA, 2011, pp. 868–871.

T. Rybina, A. Voronkov, A logical reconstruction of reachability, in: 5th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, in: Lect. Notes Comput. Sci., vol. 2890, Springer, 2003, pp. 222–237.

T. Sakata, N. Nishida, T. Sakabe, On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs, in: 20th International Workshop on Functional and Constraint Logic Programming, in: Lect. Notes Comput. Sci., vol. 6816, Springer, 2011, pp. 138–155.

P. Thati, J. Meseguer, Complete symbolic reachability analysis using back-and-forth narrowing, Theor. Comput. Sci. 366 (1–2) (2006) 163–179.

M. Veanes, N. Bjørner, A. Raschke, An SMT approach to bounded reachability analysis of model programs, in: 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, Springer, 2008, pp. 53–68.

G. Vidal, Closed symbolic execution for verifying program termination, in: IEEE 12th International Working Conference on Source Code Analysis and Manipulation, Sept 2012, pp. 34–43.

G. Vidal, Symbolic execution as a basis for termination analysis, Sci. Comput. Program. 102 (2015) 142–157

P. Viry, Equational rules for rewriting logic, Theor. Comput. Sci. 285 (2002) 487–517.

D. Walter, S. Little, C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, in: 5th International Symposium on Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2007, pp. 66–81.

S. Yovine, KRONOS: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf. 1 (1) (1997) 123–133