Abstract
In this paper we present lower bounds and rewriting algorithms for testing membership of a word in a regular language described by an extended regular expression. Motivated by intuitions from monitoring and testing, where the words to be tested (execution traces) are typically much longer than the size of the regular expressions (patterns or requirements), and by the fact that in many applications the traces are only available incrementally, on an event by event basis, our algorithms are based on an event-consumption idea: a just arrived event is “consumed” by the regular expression, i.e., the regular expression modifies itself into another expression discarding the event. We present an exponential space lower bound for monitoring extended regular expressions and argue that the presented rewriting-based algorithms, besides their simplicity and elegance, are practical and almost as good as one can hope. We experimented with and evaluated our algorithms in Maude.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
V.M. Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Journal of Theoretical Computer Science, 155(2):291–319, 1996.
V.M. Antimirov and P.D. Mosses. Rewriting extended regular expressions. Journal of Theoretical Computer Science, 143(1):51–72, 1995.
A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude: specification and programming in rewriting logic. SRI International, January 1999, http://maude.csl.sri.com.
D. Drusinsky. The Temporal Rover and the ATG Rover. In SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 323–330. Springer, 2000.
D. Giannakopoulou and K. Havelund. Automata-Based Verification of Temporal Properties on Running Programs. In Proceedings, International Conference on Automated Software Engineering (ASE’01), pages 412–416. Institute of Electrical and Electronics Engineers, 2001. Coronado Island, California.
K. Havelund and G. Roşu. Monitoring Java Programs with Java PathExplorer. In Proceedings of Runtime Verification (RV’01), volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.
K. Havelund and G. Roşu. Monitoring Programs using Rewriting. In Proceedings, International Conference on Automated Software Engineering (ASE’01), pages 135–143. Institute of Electrical and Electronics Engineers, 2001. Coronado Island, California.
K. Havelund and G. Roşu. Runtime Verification 2001, volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. Proceedings of a Computer Aided Verification (CAV’01) satellite workshop.
K. Havelund and G. Roşu. Runtime Verification 2002, volume 70(4) of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2002. Proceedings of a Computer Aided Verification (CAV’02) satellite workshop.
K. Havelund and G. Roşu. Synthesizing monitors for safety properties. In Tools and Algorithms for Construction and Analysis of Systems (TACAS’02), volume 2280 of Lecture Notes in Computer Science, pages 342–356. Springer, 2002.
S. Hirst. A new algorithm solving membership of extended regular expressions. Technical report, The University of Sydney, 1989.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980.
J.R. Knight and E.W. Myers. Super-pattern matching. Algorithmica, 13(1/2):211–243, 1995.
O. Kupferman and M. Y. Vardi. Freedom, Weakness, and Determinism: From linear-time to branching-time. In Proceedings of the IEEE Symposium on Logic in Computer Science, pages 81–92, 1998.
O. Kupferman and M. Y. Vardi. Model Checking of Safety Properties. In Proceedings of the Conference on Computer-Aided Verification, 1999.
O. Kupferman and S. Zuhovitzky. An Improved Algorithm for the Membership Problem for Extended Regular Expressions. In Proceedings of the International Symposium on Mathematical Foundations of Computer Science, 2002.
I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime Assurance Based on Formal Specifications. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999.
G. Myers. A four russians algorithm for regular expression pattern matching. Journal of the ACM, 39(4):430–448, 1992.
T. O’Malley, D. Richardson, and L. Dillon. Efficient Specification-Based Oracles for Critical Systems. In In Proceedings of the California Software Symposium, 1996.
D. J. Richardson, S. L. Aha, and T. O. O’Malley. Specification-Based Test Oracles for Reactive Systems. In Proceedings of the Fourteenth International Conference on Software Engineering, Melbourne, Australia, pages 105–118, 1992.
H. Yamamoto. An automata-based recognition algorithm for semi-extended regular expressions. In Proceedings of the International Symposium on Mathematical Foundations of Computer Science, pages 699–708, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roşu, G., Viswanathan, M. (2003). Testing Extended Regular Language Membership Incrementally by Rewriting. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_35
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive