Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Aspects of Component Software

FACS 2017: Formal Aspects of Component Software pp 78–97Cite as

Guarded Terms for Rewriting Modulo SMT

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10487))

Abstract

Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a nondeterministic environment. It seamlessly combines rewriting modulo equational theories, SMT solving, and model checking. One of the main challenges of this technique is to cope with the symbolic state-space explosion problem. This paper presents guarded terms, an approach to deal with this problem for rewriting modulo SMT. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    As an example, \(0 |_{x = 0} \equiv 0|_{x = 1}\), because \({[\![}0 |_{x = 0} {]\!]}= {[\![}0 |_{x = 1} {]\!]}= \{0\}\). But \(0 |_{x = 0} \not \equiv _g 0_{x = 1}\), because \({[\![}\theta (0 |_{x = 0}) {]\!]}= \{0\}\) and \({[\![}\theta (0 |_{x = 1}) {]\!]}= \emptyset \) for \(\theta = \{x \mapsto 0\}\), provided that \(0 \ne 1\).

  2. 2.

    For example, \(0 |_{x = 0} \equiv 0_{y = 0}\) but \((0 |_{x = 0}) |_{x = 1} \not \equiv (0 |_{y = 0}) |_{x = 1}\), because \({[\![}(0 |_{x = 0}) |_{x = 1} {]\!]}= \emptyset \) and \({[\![}(0 |_{y = 0}) |_{x = 1} {]\!]}= \{0\}\), provided that 0 and 1 are different.

  3. 3.

    Consider a set of equations E that replace any constraint in a guarded term by its negation. Then, \(0 |_{ false } \equiv _E 0 |_{\lnot false }\), but clearly \({[\![}0 |_{ false } {]\!]}\ne {[\![}0 |_{\lnot false } {]\!]}\).

  4. 4.

    The specification of ALL has been omitted in the rule. ALL represents the entire configuration in the left hand side.

  5. 5.

    The monus operator is defined by: \(a \texttt { monus } b = \max (a-b, 0)\).

  6. 6.

    The function nextDeadlineWaiting(ALL,O,T2) returns a constraint stating that the timeToDeadline of all servers, except O, is at least T2.

  7. 7.

    The functions delta-global and delta-servers model the time lapse; that is, variables in servers and the queue are accordingly increased or decreased (by 1) based on the current state.

References

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

    Article  MATH  Google Scholar 

  2. Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl (2013)

    Google Scholar 

  3. Bae, K., Ölveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94–109. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_7

    Chapter  Google Scholar 

  4. Bae, K., Ölveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Sci. Comput. Program. 77(12), 1235–1271 (2012)

    Article  MATH  Google Scholar 

  5. Bae, K., Rocha, C.: A Note on Guarded Terms for Rewriting Modulo SMT, July 2017. http://sevlab.postech.ac.kr/~kmbae/rew-smt

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

    Article  MathSciNet  MATH  Google Scholar 

  7. Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: RTSS, pp. 295–304. IEEE (2000)

    Google Scholar 

  8. Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224 (2008)

    Google Scholar 

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

    Article  Google Scholar 

  10. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_23

    Chapter  Google Scholar 

  11. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  12. Dowek, G., Muñoz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. Electron. Proc. Theor. Comput. Sci. 18, 77–91 (2010)

    Article  Google Scholar 

  13. Lal, A., Qadeer, S., Lahiri, S.: Corral: a solver for reachability modulo theories. Technical report MSR-TR-2012-9, Microsoft Research, January 2012

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7–8), 721–781 (2012)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  17. Ölveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357–372. Springer, Heidelberg (2006). doi:10.1007/11693017_26

    Chapter  Google Scholar 

  18. Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. Ph.D. thesis, University of Illinois, December 2012

    Google Scholar 

  19. Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269–297 (2017)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

The first author was supported by the Basic Science Research Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Education (2016R1D1A1B03935275). The second author has been supported in part by the EPIC project funded by the Administrative Department of Science, Technology and Innovation of Colombia (Colciencias) under contract 233-2017.

Author information

Authors and Affiliations

  1. Pohang University of Science and Technology, Pohang, South Korea

    Kyungmin Bae

  2. Pontificia Universidad Javeriana, Cali, Colombia

    Camilo Rocha

Authors
  1. Kyungmin Bae
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Camilo Rocha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kyungmin Bae .

Editor information

Editors and Affiliations

  1. University of Minho, Braga, Portugal

    José Proença

  2. Swinburne University of Technology, Hawthorn, Victoria, Australia

    Markus Lumpe

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bae, K., Rocha, C. (2017). Guarded Terms for Rewriting Modulo SMT. In: Proença, J., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2017. Lecture Notes in Computer Science(), vol 10487. Springer, Cham. https://doi.org/10.1007/978-3-319-68034-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68034-7_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68033-0

  • Online ISBN: 978-3-319-68034-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation