{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:16Z","timestamp":1760586436028,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727934"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72794-1_12","type":"book-chapter","created":{"date-parts":[[2007,6,25]],"date-time":"2007-06-25T11:13:58Z","timestamp":1182770038000},"page":"211-230","source":"Crossref","is-referenced-by-count":6,"title":["Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants"],"prefix":"10.1007","author":[{"given":"Slim","family":"Kallel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anis","family":"Charfi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mira","family":"Mezini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Jmaiel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"Object-Oriented and Internet-Based Technologies","author":"G. Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C.V., Loingtier, J.M., Irwin, J.: Aspect-Oriented Programming. In: Weske, M., Liggesmeyer, P. (eds.) NODe 2004. LNCS, vol.\u00a03263, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"key":"12_CR2","volume-title":"The Z notation: a reference manual","author":"M. Spivey","year":"1992","unstructured":"Spivey, M.: The Z notation: a reference manual, 2nd edn. Prentice Hall International Ltd., Hertfordshire (1992)","edition":"2"},{"key":"12_CR3","unstructured":"Meisels, I., Saaltink, M.: The Z\/EVES Reference Manual (for Version 1.5). Reference manual, ORA Canada (1997)"},{"key":"12_CR4","unstructured":"Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Darmstadt University of Technology, Darmstadt, Germany (1961)"},{"key":"12_CR5","volume-title":"The Way of Z: Practical Programming with Formal Methods","author":"J. Jacky","year":"1997","unstructured":"Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1997)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Concurrent Object-Oriented Programming and Petri Nets","year":"2001","unstructured":"Agha, G.A., De Cindio, F., Rozenberg, G. (eds.): Concurrent Object-Oriented Programming and Petri Nets. LNCS, vol.\u00a02001. Springer, Heidelberg (2001)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"G. Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An Overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 327\u2013353. Springer, Heidelberg (2001)"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1023\/A:1021798709301","volume":"24","author":"M.C. Pellegrini","year":"2003","unstructured":"Pellegrini, M.C., Riveill, M.: Component Management in a Dynamic Architecture. The Journal of Supercomputing\u00a024, 151\u2013159 (2003)","journal-title":"The Journal of Supercomputing"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/582128.582135","volume-title":"Proceedings of the first workshop on Self-healing systems","author":"I. Georgiadis","year":"2002","unstructured":"Georgiadis, I., Magee, J., Kramer, J.: Self-organising software architectures for distributed systems. In: Proceedings of the first workshop on Self-healing systems, pp. 33\u201338. ACM Press, New York (2002)"},{"key":"12_CR10","unstructured":"Medvidovic, N., Egyed, A., Gruenbacher, P.: Stemming Architectural Erosion by Coupling Architectural Discovery and Recovery. In: Proc. of the 2nd International Software Requirements to Architectures Workshop, Portland, Oregon (2003)"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/1167473.1167484","volume-title":"Proc. of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications","author":"C. Bockisch","year":"2006","unstructured":"Bockisch, C., Kanthak, S., Haupt, M., Arnold, M., Mezini, M.: Efficient control flow quantification. In: Proc. of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pp. 125\u2013138. ACM Press, New York (2006)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/1167473.1167483","volume-title":"Proc. of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications","author":"C. Bockisch","year":"2006","unstructured":"Bockisch, C., Arnold, M., Dinkelaker, T., Mezini, M.: Adapting virtual machine techniques for seamless aspect support. In: Proc. of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pp. 109\u2013124. ACM Press, New York (2006)"},{"key":"12_CR13","volume-title":"Aspect Oriented Refactoring","author":"R. Laddad","year":"2006","unstructured":"Laddad, R.: Aspect Oriented Refactoring. Addison-Wesley Professional, Reading (2006)"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/508386.508388","volume-title":"Proc. of the 1st international conference on Aspect-oriented software development","author":"M. Shomrat","year":"2002","unstructured":"Shomrat, M., Yehudai, A.: Obvious or not?: regulating architectural decisions using aspect-oriented programming. In: Proc. of the 1st international conference on Aspect-oriented software development, pp. 3\u20139. ACM Press, New York (2002)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-45821-2_11","volume-title":"Generative Programming and Component Engineering","author":"R. Douence","year":"2002","unstructured":"Douence, R., Fradet, P., Sudholt, M.: A Framework for the Detection and Resolution of Aspect Interactions. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol.\u00a02487, pp. 173\u2013188. Springer, Heidelberg (2002)"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1109\/ICALT.2003.1215093","volume-title":"Proc. of the 3rd IEEE International Conference on Advanced Learning Technologies","author":"D. Gasevic","year":"2003","unstructured":"Gasevic, D., Devedzic, D.: Software Support for Teaching Petri Nets: P3. In: Proc. of the 3rd IEEE International Conference on Advanced Learning Technologies, Athens, Greece, pp. 300\u2013301. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/32.825767","volume":"26","author":"N. Medvidovic","year":"2000","unstructured":"Medvidovic, N., Taylor, R.N.: A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering\u00a026, 70\u201393 (2000)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Kacem, M.H., Jmaiel, M., Kacem, A.H., Drira, K.: Evaluation and Comparison of ADL Based Approaches for the Description of Dynamic of Software Architectures. In: Proc. of the Seventh International Conference on Enterprise Information Systems, Miami, pp. 189\u2013195 (2005)","DOI":"10.5220\/0002524701890195"},{"key":"12_CR19","unstructured":"Endler, M., Wei, J.: Programming generic dynamic reconfigurations for distributed applications. In: Proc. of the International Workshop on Configurable Distributed Systems, pp. 68\u201379 (1992)"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/226241.226244","volume":"4","author":"G. Abowd","year":"1995","unstructured":"Abowd, G., Allen, R., Garlan, D.: Formalizing style to understand descriptions of software architecture. ACM Transactions on Software Engineering and Methodology\u00a04, 319\u2013364 (1995)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1109\/ASE.2002.1115028","volume-title":"Proc. of the 17th IEEE International Conference on Automated Software Engineering","author":"N. Aguirre","year":"2002","unstructured":"Aguirre, N., Maibaum, T.: A Temporal Logic Approach to the Specification of Reconfigurable Component-Based Systems. In: Proc. of the 17th IEEE International Conference on Automated Software Engineering, Edinburgh, Scotland, pp. 271\u2013274. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1109\/32.708567","volume":"24","author":"D.L. M\u00e9tayer","year":"1998","unstructured":"M\u00e9tayer, D.L.: Describing software architecture styles using graph grammars. IEEE Transactions on Software Engineering\u00a024, 521\u2013553 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/96709.96717","volume-title":"Proc. of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"G. Berry","year":"1990","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. In: Proc. of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 81\u201394. ACM Press, New York (1990)"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1049\/ip-sen:20030132","volume":"150","author":"G.H. Hilderink","year":"2003","unstructured":"Hilderink, G.H.: Graphical modelling language for specifying concurrency based on CSP. IEE Proceedings - Software\u00a0150, 108\u2013120 (2003)","journal-title":"IEE Proceedings - Software"},{"key":"12_CR25","first-page":"1","volume":"31","author":"F. Oquendo","year":"2006","unstructured":"Oquendo, F.: \u03c0-method: a model-driven formal method for architecture-centric software engineering. SIGSOFT Software Engineering Notes\u00a031, 1\u201313 (2006)","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"12_CR26","volume-title":"Proc. of the International Conference of Formal Engineering Methods","author":"A. Galloway","year":"1997","unstructured":"Galloway, A., Stoddart, B.: An operational semantics for ZCCS. In: Proc. of the International Conference of Formal Engineering Methods, IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"12_CR27","first-page":"31","volume-title":"Proc. of the 15th International Conference on Computer Safety, Reliability and Security","author":"M. Heisel","year":"1996","unstructured":"Heisel, M., Shl, C.: Formal specification of safety-critical software with Z and real-time CSP. In: Proc. of the 15th International Conference on Computer Safety, Reliability and Security, Vienna, Austria, pp. 31\u201346. Springer, Heidelberg (1996)"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-63533-5_4","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"G. Smith","year":"1997","unstructured":"Smith, G.: A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. In: Fitzgerald, J., Jones, C.B, Lucas, P. (eds.) FME 1997. LNCS, vol.\u00a01313, pp. 62\u201381. Springer, Heidelberg (1997)"},{"key":"12_CR29","unstructured":"Bussow, R., Geisler, R., Grieskamp, W., Klar, M.: The \u03bcSZ Notation Version 1.0. Technical report, TU Berlin, Gemany (1997)"},{"key":"12_CR30","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/S0164-1212(02)00087-0","volume":"71","author":"X. He","year":"2004","unstructured":"He, X., Yu, H., Shi, T., Ding, J., Deng, Y.: Formally analyzing software architectural specifications using SAM. Journal System Software\u00a071, 11\u201329 (2004)","journal-title":"Journal System Software"},{"key":"12_CR31","first-page":"327","volume":"1","author":"A. Regayeg","year":"2006","unstructured":"Regayeg, A., Kallel, S., Kacem, A.H., Jmaiel, M.: ForMAAD Method: An Experimental Design for Air Traffic Control. International Transactions on Systems Science and Applications\u00a01, 327\u2013334 (2006)","journal-title":"International Transactions on Systems Science and Applications"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Rodriguez-Fortiz, M., Parets-Llorca, J.: Using predicate temporal logic and coloured Petri nets to specifying integrity restrictions in the structural evolution of temporal active systems. In: Proc. of the international symposium on principles of software evolution, pp. 83\u201387 (2000)","DOI":"10.1109\/ISPSE.2000.913225"},{"key":"12_CR33","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1109\/ICIS-COMSAR.2006.41","volume-title":"Proc. of the 5th IEEE\/ACIS International Conference on Computer and Information Science","author":"S. Ramkarthik","year":"2006","unstructured":"Ramkarthik, S., Zhang, C.: Generating Java Skeletal Code with Design Contracts from Specifications in a Subset of Object Z. In: Proc. of the 5th IEEE\/ACIS International Conference on Computer and Information Science, Honolulu, Hawaii, pp. 405\u2013411. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"12_CR34","first-page":"393","volume-title":"Proc. of the 22nd International Computer Software and Applications Conference","author":"X. Jia","year":"1998","unstructured":"Jia, X., Skevoulis, S.: Code Synthesis Based on Object-Oriented Design Models and Formal Specifications. In: Proc. of the 22nd International Computer Software and Applications Conference, Washington, DC, pp. 393\u2013399. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"12_CR35","volume-title":"Proc. of the Grand finals of the ACM Student Research Competition","author":"E. Bodden","year":"2005","unstructured":"Bodden, E.: Efficient and Expressive Runtime Verification for Java. In: Proc. of the Grand finals of the ACM Student Research Competition, San Francisco, ACM Press, New York (2005)"},{"key":"12_CR36","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/1181775.1181802","volume-title":"Proc. of the 14th ACM SIGSOFT international symposium on Foundations of software engineering","author":"S. Maoz","year":"2006","unstructured":"Maoz, S., Harel, D.: From multi-modal scenarios to code: compiling LSCs into aspectJ. In: Proc. of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 219\u2013230. ACM Press, New York (2006)"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/11531142_10","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"K. Ostermann","year":"2005","unstructured":"Ostermann, K., Mezini, M., Bockisch, C.: Expressive Pointcuts for Increased Modularity. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 214\u2013240. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72794-1_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T17:10:52Z","timestamp":1737133852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72794-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727934"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72794-1_12","relation":{},"subject":[]}}