Copyright © 2007 The Institute of Electronics, Information and Communication Engineers
Regular Section -- Papers -- Automata and Formal Language Theory |
A Labeled Transition Model A-LTS for History-Based Aspect Weaving and Its Expressive Power
1 The authors are with the Graduate School of Information Science, Nara Institute of Science and Technology, Ikoma-shi, 630–0101 Japan. E-mail: isao-y{at}is.naist.jp, E-mail: y-takata{at}is.naist.jp and E-mail: seki{at}is.naist.jp
This paper proposes an event-based transition system called A-LTS. An A-LTS is a simple system consisting of two agents, a basic program and a monitor. The monitor observes the behavior of the basic program and if the behavior matches some pre-defined pattern, then the monitor interrupts the execution of the basic program and possibly triggers the execution of another specific program. An A-LTS models a common feature found in recent software technologies such as Aspect-Oriented Programming (AOP), history-based access control and active database. We investigate the expressive power of A-LTS and show that it is strictly stronger than finite state machines and strictly weaker than pushdown automata (PDA). This implies that the model checking problem for A-LTS is decidable. It is also shown that the expressive power of A-LTS, linear context-free grammar and deterministic PDA are mutually incomparable. We also discuss the relationship between A-LTS and pointcut/advice in AOP.
Key Words: labeled transition system, pushdown automaton, formal model, aspect-oriented programming, AspectJ
Manuscript received August 3, 2006. Manuscript revised December 1, 2006.
References
[1] R. Alur, K. Etessami, and M. Yannakakis, "Analysis of recursive state machines," 13th Conference on Computer Aided Verification (CAV 2001), LNCS 2102, pp.207–220, Paris, France, July 2001.
[2] M. Abadi and C. Fournet, "Access control based on execution history," Network & Distributed System Security Symp., pp.107–121, San Diego, USA, Feb. 2003.
[3] AspectJ Team, http://aspectj.org/
[4] M. Benedikt, P. Godefroid, and T. Reps, "Model checking of unrestricted hierarchical state machine," 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), LNCS 2076, pp.652–666, Crete, Greece, July 2001.
[5] G. Bruns, R. Jagadeesan, A. Jeffrey, and J. Riely, "µABC: A minimal aspect calculus," 15th International Conference on Concurrency Theory (CONCUR 2004), LNCS 3170, pp.209–224 London, England, Aug. 2004.
[6] E.M. Clarke, Jr., O. Grumberg, and D. Peled, Model Checking, MIT Press, 2000.
[7] R. Douence, O. Motelet, and M. Sudholt, "A formal definition of crosscuts," 3rd International Conference on Metalevel Architectures and Separation of Crosscutting Concerns (REFLECTION 2001), LNCS 2192, pp.170–186, Kyoto, Japan, Sept. 2001.
[8] Y. Endoh, H. Masuhara, and A. Yonezawa, "Continuation join point," Foundations of Aspect-Oriented Languages Workshop 2006(FOAL 2006), pp.1–10, Bonn, Germany, March 2006.
[9] J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, "Efficient algorithms for model-checking pushdown systems," 12th Conference on Computer Aided Verification (CAV 2000), LNCS 1855, pp.232–247, Chicago, USA, July 2000.
[10] P.W. Fong, "Access control by tracking shallow execution history," IEEE Security & Privacy, pp.43–55, Oakland, USA, May 2004.
[11] P. Linz, An Introduction to Formal Languages and Automata, pp.196–198, Jones and Bartlett Publishers, Sudbury, 2001.
[12] H. Masuhara and G. Kiczales, "Modeling crosscutting in aspect-oriented mechanisms," 17th European Conference on Object-Oriented Programming (ECOOP 2003), LNCS 2743, pp.2–28, Darmstadt, Germany, July 2003.
[13] M. Mukund, "From global specifications to distributed implementations," in Synthesis and Control of Discrete Event Systems, ed. B. Caillaud, P. Darondeau, L. Lavagno, and X. Xie, pp.19–35, Kluwer Academic Publishers, 2002.
[14] S. Nakajima and T. Tamai, "Aspect-oriented software design with a variant of UML/STD," 5th International Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM 2006), pp.44–50, Shanghai, China, May 2006.
[15] N. Nitta, Y. Takata, and H. Seki, "An efficient security verification method for programs with stack inspection," 8th ACM Computer & Communications Security, pp.68–77, Philadelphia, USA, Nov. 2001.
[16] N.W. Paton and O. Diaz, "Active database systems," ACM Comput. Surv., vol.31, no.1, pp.63–103, March 1999.
[17] F.B. Schneider, "Enforceable security policies," ACM Trans. on Information & System Security, vol.3, no.1, pp.30–50, Feb. 2000.
[18] D. Walker, S. Zdancewic, and J. Ligatti, "A theory of aspects," 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), pp.127–139, Uppsala, Sweden, Aug. 2003.
[19] I. Walukiewicz, "Pushdown processes: Games and model checking," 8th Conference on Computer Aided Verification (CAV '96), LNCS 1102, pp.62–74, New Brunswick, July 1996.
[20] M. Wand, G. Kiczales, and C. Dutchyn, "A semantics for advice and dynamic join points in aspect-oriented programming," ACM Trans. on Programming Languages and Systems (TOPLAS), vol.3, no.5, pp.890–910, Sept. 2004.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||||