{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:59:37Z","timestamp":1743040777952,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319246437"},{"type":"electronic","value":"9783319246444"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24644-4_11","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T01:34:39Z","timestamp":1443058479000},"page":"159-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Incremental Realization of Safety Requirements: Non-determinism vs. Modularity"],"prefix":"10.1007","author":[{"given":"Ali","family":"Ebnenasir","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters\u00a021, 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Attie, P., Emerson, A.: Synthesis of concurrent programs for an atomic read\/write model of computation. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a023(2) (March 2001). An extended abstract appeared at the ACM Symposium on Principles of Distributed Computing (1996)","DOI":"10.1145\/383043.383044"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1462187.1462192","volume":"4","author":"B. Bonakdarpour","year":"2009","unstructured":"Bonakdarpour, B., Ebnenasir, A., Kulkarni, S.S.: Complexity results in revising UNITY programs. ACM Transactions on Autonomous and Adaptive Systems\u00a04(1), 1\u201328 (2009)","journal-title":"ACM Transactions on Autonomous and Adaptive Systems"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-540-92221-6_26","volume-title":"Principles of Distributed Systems","author":"B. Bonakdarpour","year":"2008","unstructured":"Bonakdarpour, B., Kulkarni, S.S.: Revising distributed UNITY programs is NP-complete. In: Baker, T.P., Bui, A., Tixeuil, S. (eds.) OPODIS 2008. LNCS, vol.\u00a05401, pp. 408\u2013427. Springer, Heidelberg (2008)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: POPL 2000: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 54\u201366 (2000)","DOI":"10.1145\/325694.325703"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Djoko, S.D., Douence, R., Fradet, P.: Aspects preserving properties. In: ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM), pp. 135\u2013145 (2008)","DOI":"10.1145\/1328408.1328429"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/11795490_22","volume-title":"Principles of Distributed Systems","author":"A. Ebnenasir","year":"2006","unstructured":"Ebnenasir, A., Kulkarni, S.S., Bonakdarpour, B.: Revising UNITY programs: Possibilities and limitations. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 275\u2013290. Springer, Heidelberg (2006)"},{"key":"11_CR8","unstructured":"Emerson, E.A.: chapter 16: Temporal and Modal Logics. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 995\u20131067. Elsevier Science Publishers B.V (1990)"},{"key":"11_CR9","unstructured":"Garey, M., Johnson, D.: Computers and Interactability: A guide to the theory of NP-completeness. W.H. Freeman and Company (1979)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-71209-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Goldman","year":"2007","unstructured":"Goldman, M., Katz, S.: Maven: Modular aspect verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 308\u2013322. Springer, Heidelberg (2007)"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/S1571-0661(04)80411-0","volume":"66","author":"H. Hansen","year":"2002","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. Electronic Notes in Theoretical Computer Science\u00a066(2), 178\u2013193 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1109\/70.988975","volume":"18","author":"M.V. Iordache","year":"2002","unstructured":"Iordache, M.V., Moody, J.O., Antsaklis, P.J.: Synthesis of deadlock prevention supervisors using Petri Nets. IEEE Transactions on Robotics and Automation\u00a018(1), 59\u201368 (2002)","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Khatchadourian, R., Dovland, J., Soundarajan, N.: Enforcing behavioral constraints in evolving aspect-oriented programs. In: Proceedings of the 7th Workshop on Foundations of Aspect-oriented Languages (FOAL), pp. 19\u201328 (2008)","DOI":"10.1145\/1394496.1394499"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP \u201997 - Object-Oriented Programming","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: Ak\u015fit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Kiczales, G., Rivieres, J.D.: The Art of the Metaobject Protocol. MIT Press, Cambridge (1991)","DOI":"10.7551\/mitpress\/1405.001.0001"},{"issue":"2","key":"11_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1217295.1217296","volume":"16","author":"S. Krishnamurthi","year":"2007","unstructured":"Krishnamurthi, S., Fisler, K.: Foundations of incremental aspect model-checking. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a016(2), 7 (2007)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"issue":"6","key":"11_CR17","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/1041685.1029916","volume":"29","author":"S. Krishnamurthi","year":"2004","unstructured":"Krishnamurthi, S., Fisler, K., Greenberg, M.: Verifying aspect advice modularly. ACM SIGSOFT Software Engineering Notes\u00a029(6), 137\u2013146 (2004)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"11_CR18","unstructured":"Kulkarni, S.S.: Component-based design of fault-tolerance. PhD thesis, Ohio State University, OH, USA (1999)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45352-0_9","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"S.S. Kulkarni","year":"2000","unstructured":"Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol.\u00a01926, pp. 82\u201393. Springer, Heidelberg (2000)"},{"issue":"4","key":"11_CR20","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1109\/TDSC.2005.52","volume":"2","author":"S.S. Kulkarni","year":"2005","unstructured":"Kulkarni, S.S., Ebnenasir, A.: The effect of the safety specification model on the complexity of adding masking fault-tolerance. IEEE Transaction on Dependable and Secure Computing\u00a02(4), 348\u2013355 (2005)","journal-title":"IEEE Transaction on Dependable and Secure Computing"},{"issue":"6","key":"11_CR21","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1109\/TC.2003.1204828","volume":"52","author":"P.K. McKinley","year":"2003","unstructured":"McKinley, P.K., Padmanabhan, U.I., Ancha, N., Sadjadi, S.M.: Composable proxy services to support collaboration on the mobile internet. IEEE Transactions on Computers\u00a052(6), 713\u2013726 (2003)","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"11_CR22","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TSE.1979.234169","volume":"5","author":"D.L. Parnas","year":"1979","unstructured":"Parnas, D.L.: Designing software for ease of extension and contraction. IEEE Transactions on Software Engineering\u00a05(2), 128\u2013138 (1979)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR23","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1007\/978-3-642-35179-2_5","volume":"6","author":"A.-E.B. Salem","year":"2012","unstructured":"Salem, A.-E.B., Duret-Lutz, A., Kordon, F.: Model checking using generalized testing automata. Transactions on Petri Nets and Other Models of Concurrency\u00a06, 94\u2013122 (2012)","journal-title":"Transactions on Petri Nets and Other Models of Concurrency"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Smith, D.: Requirement enforcement by transformation automata. In: Sixth Workshop on Foundations of Aspect-Oriented Languages (FOAL), pp. 5\u201315 (2007)","DOI":"10.1145\/1233833.1233835"},{"issue":"7","key":"11_CR25","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1109\/9.599972","volume":"42","author":"R.S. Sreenivas","year":"1997","unstructured":"Sreenivas, R.S.: On the existence of supervisory policies that enforce liveness in discrete-event dynamic systems modeled by controlled Petri Nets. IEEE Transactions on Automatic Control\u00a042(7), 928\u2013945 (1997)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Thaker, S., Batory, D.S., Kitchin, D., Cook, W.R.: Safe composition of product lines. In: 6th International Conference on Generative Programming and Component Engineering (GPCE), pp. 95\u2013104 (2007)","DOI":"10.1145\/1289971.1289989"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 139\u2013154. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24644-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,23]],"date-time":"2019-09-23T20:04:46Z","timestamp":1569269086000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24644-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319246437","9783319246444"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24644-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}