{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:22:25Z","timestamp":1768008145446,"version":"3.49.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2009,9,1]],"date-time":"2009-09-01T00:00:00Z","timestamp":1251763200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1007\/s11390-009-9269-5","type":"journal-article","created":{"date-parts":[[2009,9,28]],"date-time":"2009-09-28T11:22:01Z","timestamp":1254136921000},"page":"949-961","source":"Crossref","is-referenced-by-count":9,"title":["Aspect-Oriented Modeling and Verification with Finite State Machines"],"prefix":"10.1007","volume":"24","author":[{"given":"Dian-Xiang","family":"Xu","sequence":"first","affiliation":[]},{"given":"Omar","family":"El-Ariss","sequence":"additional","affiliation":[]},{"given":"Wei-Feng","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Lin-Zhang","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,9,28]]},"reference":[{"key":"9269_CR1","doi-asserted-by":"crossref","unstructured":"Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold W G. An overview of AspectJ. In Proc. ECOOP2001, Budapest, Hungary, June 18{22, 2001, pp.327\u2013353.","DOI":"10.1007\/3-540-45337-7_18"},{"key":"9269_CR2","doi-asserted-by":"crossref","unstructured":"Kiczales G, Lamping J, Mendhekar A, Maeda C, Lopes C V, Loingtier J M, Irwin J. Aspect-oriented programming. In Proc. ECOOP1997, Jyv\u00e4skyl\u00e4, Finland, June 9\u201313, 1997, pp.220\u2013242.","DOI":"10.21236\/ADA417906"},{"key":"9269_CR3","doi-asserted-by":"crossref","unstructured":"Rinard M, Salcianu A, Bugrara S. A classification system and analysis for aspect-oriented programs. In Proc. FSE 2004, New Delhi, India, Feb. 5\u20137, 2004, pp.147\u2013158.","DOI":"10.1145\/1029894.1029917"},{"key":"9269_CR4","doi-asserted-by":"crossref","unstructured":"Sullivan K, Griswold W G, Song Y, Cai Y, Shonle M, Tewari N, Rajan H. Information hiding interfaces for aspect-oriented design. In Proc. ESEC\/FSE 2005, Lisbon, Portugal, Sept. 5\u20139, 2005, pp.166\u2013175.","DOI":"10.1145\/1081706.1081734"},{"key":"9269_CR5","doi-asserted-by":"crossref","unstructured":"Xu D, Xu W. State-based incremental testing of aspectoriented programs. In Proc. the Fifth International Conf. Aspect-Oriented Software Development (AOSD2006), Bonn, Germany, March 20\u201324, 2006, pp.180\u2013189.","DOI":"10.1145\/1119655.1119680"},{"key":"9269_CR6","doi-asserted-by":"crossref","unstructured":"Katz S. Aspect Categories and Classes of Temporal Properties. Transactions on Aspect-Oriented Software Development I, Rashid A, Aksit M (eds.), LNCS 3880, 2006, pp.106\u2013134.","DOI":"10.1007\/11687061_4"},{"key":"9269_CR7","unstructured":"Schauerhuber A, Schwinger W, Retschitzegger W, Wimmer M. A survey on aspect-oriented modeling approaches. Technical Report, Vienna University of Technology, January 2006, http:\/\/www.wit.at\/people\/schauerhuber\/publications\/aom-Survey\/AOMSurvey2006-01-30.pdf ."},{"key":"9269_CR8","doi-asserted-by":"crossref","unstructured":"Xu D, Alsmadi I, Xu W. Model checking aspect-oriented design specification. In Proc. the 31st Annual International Computer Software and Applications Conference (COMPSAC2007), Beijing, China, July 23{27, 2007, pp.491\u2013500.","DOI":"10.1109\/COMPSAC.2007.152"},{"key":"9269_CR9","unstructured":"Magee J, Kramer J. Concurrency: State Models and Java Programs. Second Edition, John Wiley & Sons Ltd, 2006."},{"key":"9269_CR10","unstructured":"Binder R V. Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison-Wesley, 2000."},{"key":"9269_CR11","unstructured":"UML 2.0 superstructure and infrastructure specification. http:\/\/www.omg.org\/technology\/documents\/formal\/uml.htm ."},{"key":"9269_CR12","unstructured":"Alexander R T, Bieman J M, Andrews A A. Towards the systematic testing of aspect-oriented programs. Technical Report, Colorado State University, 2004, http:\/\/www.cs.colostate.edu\/!~rta\/publications\/CS-04-105.pdf ."},{"key":"9269_CR13","unstructured":"Aldawud O, Bader F, Elrad T. Weaving with statecharts. In The Second International Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30\u2013Oct. 4, 2002."},{"key":"9269_CR14","unstructured":"Chavez C, Lucena C. A meta-model for aspect-oriented modeling. In The 2nd Int. Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30\u2013Oct. 4, 2002."},{"key":"9269_CR15","unstructured":"Clarke S, Walker R J. Generic Aspect-Oriented Design with Theme\/UML. Aspect-Oriented Software Development. Filman R E, Elrad T, Clarke S, Aksit M (eds.), Boston: Addison-Wesley, 2005, pp.425\u2013458."},{"key":"9269_CR16","unstructured":"Han Y, Kniesel G, Cremers A B. A meta model and modeling notation for AspectJ. In The 5th Workshop on Aspect-Oriented Modeling with UML, in conjunction with UML2004, Lisbon, Portugal, October 11\u201315, 2004."},{"key":"9269_CR17","unstructured":"Pawlak R, Duchien L, Florin G, Legond-Aubry F, Seinturier L, Martelli L. A UML notation for aspect-oriented software design. In The 1st Int. Workshop on Aspect-Oriented Modeling with UML, in conjunction with AOSD2002, Enschede, The Netherlands, April 22\u201326, 2002."},{"key":"9269_CR18","doi-asserted-by":"crossref","unstructured":"Stein D, Hanenberg S, Unland R. An UML-based aspect-oriented design notation. In Proc. the 1st Int. Conf. Aspect-Oriented Software Development (AOSD2002), Enschede, The Netherlands, April 22\u201326, 2002, pp.106\u2013112.","DOI":"10.1145\/508397.508399"},{"key":"9269_CR19","unstructured":"Stein D, Hanenberg S, Unland R. On representing join points in the UML. In The Second International Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30\u2013Oct. 4, 2002."},{"key":"9269_CR20","unstructured":"Zavaleta E B, Fuster G G, Morillo J L. An approach to aspect modeling with UML 2.0. In The 5th Workshop on Aspect-Oriented Modeling with UML, in conjunction with UML2004, Lisbon, Portugal, October 11\u201315, 2004."},{"key":"9269_CR21","unstructured":"Elrad T, Aldawud O, Bader A. Expressing Aspects Using UML Behavior and Structural Diagrams. Aspect-Oriented Software Development, Filman et al. (eds.), Boston: Addison-Wesley, 2005, pp.459\u2013478."},{"issue":"4","key":"9269_CR22","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1109\/TSE.2006.40","volume":"32","author":"D Xu","year":"2006","unstructured":"Xu D, Nygard K. Threat-driven modeling and verification of secure software using aspect-oriented Petri nets. IEEE Trans. Software Engineering. April 2006, 32(4): 265\u2013278.","journal-title":"IEEE Trans. Software Engineering. April"},{"key":"9269_CR23","doi-asserted-by":"crossref","unstructured":"Ubayashi N, Tamai T. Aspect-oriented programming with model checking. In Proc. the First International Conf. Aspect-Oriented Software Development (AOSD2002), Enschede, The Netherlands, April 22\u201326, 2002, pp.148\u2013154.","DOI":"10.1145\/508386.508405"},{"key":"9269_CR24","doi-asserted-by":"crossref","unstructured":"Denaro G, Monga M. An experience on verification of aspect properties. In International Workshop on Principles of Software Evolution (IWPSE 2001), Vienna, Austria, Sept. 10\u201311, 2001, pp.186\u2013189.","DOI":"10.1145\/602461.602506"},{"key":"9269_CR25","doi-asserted-by":"crossref","unstructured":"Nelson T, Cowan D D, Alencar P S C. Supporting formal verification of crosscutting concerns. In Proc. Reflection, Kyoto, Japan, Sept. 25\u201328, 2001, pp.153\u2013169.","DOI":"10.1007\/3-540-45429-2_12"},{"key":"9269_CR26","doi-asserted-by":"crossref","unstructured":"Krishnamurthi S, Fisler K, Greenberg M. Verifying aspect advice modularly. In Proc. the 12th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2004), Newport Beach, USA, Oct. 31\u2013Nov. 6, 2004, pp.137\u2013146.","DOI":"10.1145\/1029894.1029916"},{"key":"9269_CR27","doi-asserted-by":"crossref","unstructured":"Katz S, Sihman M. Aspect-validation using model-checking. In Proc. the International Symposium on Verification, in honor of Zohar Manna, LNCS 2772, Springer-Verlag, 2003, pp.389\u2013411, Also early version in FOAL 2003.","DOI":"10.1007\/978-3-540-39910-0_18"},{"key":"9269_CR28","unstructured":"Sihman M, Katz S. Model checking applications of aspects and superimpositions. In Proc. Foundations of Aspect-Oriented Languages, Bonn, Germany, March 20\u201324, 2003, pp.51\u201360."},{"key":"9269_CR29","doi-asserted-by":"crossref","unstructured":"Hatcliff J, Dwyer M. Using the Bandera tool set to model-check properties of concurrent Java software. In Proc. the 12th Int. Conf. Concurrency Theory (CONCUR2001), Aalborg, Denmark, LNCS 2154, Larsen K G, Nielsen M (eds.), Springer-Verlag, Aug. 20\u201325, 2001, pp.39\u201358.","DOI":"10.1007\/3-540-44685-0_5"},{"key":"9269_CR30","doi-asserted-by":"crossref","unstructured":"Katz E, Katz S. Verifying scenario-based aspect specifications. In Proc. the International Symposium of Formal Methods Europe, Newcastle, UK, July 18\u201322, 2005, pp.432\u2013447.","DOI":"10.1007\/11526841_29"},{"key":"9269_CR31","unstructured":"Goldman M, Katz S. Modular generic verification of LTL properties for aspects. In Proc. Foundations of Aspect Languages Workshop (FOAL2006), Bonn, Germany, March 20\u201324, 2006."},{"key":"9269_CR32","doi-asserted-by":"crossref","unstructured":"Andrews J H. Process-algebraic foundations of aspect-oriented programming. In Proc. Reflection, Kyoto, Japan Sept. 25\u201328, 2001, pp.187\u2013209.","DOI":"10.1007\/3-540-45429-2_14"},{"key":"9269_CR33","unstructured":"Xu J, Rajan H, Sullivan K. Aspect reasoning by reduction to implicit invocation. In Proc. Foundations of Aspect-Oriented Languages, Lancaster, UK, March 23, 2004."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9269-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-009-9269-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9269-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T11:25:12Z","timestamp":1739359512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-009-9269-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["9269"],"URL":"https:\/\/doi.org\/10.1007\/s11390-009-9269-5","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9]]}}}