{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:00:24Z","timestamp":1742382024242},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2008,7,31]],"date-time":"2008-07-31T00:00:00Z","timestamp":1217462400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2008,10]]},"DOI":"10.1007\/s10009-008-0083-0","type":"journal-article","created":{"date-parts":[[2008,7,30]],"date-time":"2008-07-30T12:02:54Z","timestamp":1217419374000},"page":"455-471","source":"Crossref","is-referenced-by-count":25,"title":["FTSyn: a framework for automatic synthesis of fault-tolerance"],"prefix":"10.1007","volume":"10","author":[{"given":"Ali","family":"Ebnenasir","sequence":"first","affiliation":[]},{"given":"Sandeep S.","family":"Kulkarni","sequence":"additional","affiliation":[]},{"given":"Anish","family":"Arora","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,7,31]]},"reference":[{"key":"83_CR1","unstructured":"A framework for automatic synthesis of fault-tolerance. http:\/\/www.cse.msu.edu\/~sandeep\/software\/Code\/synthesis-framework\/"},{"key":"83_CR2","unstructured":"Spin language reference. http:\/\/spinroot.com\/spin\/Man\/promela.html"},{"key":"83_CR3","doi-asserted-by":"crossref","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. Inform. Process. Lett. 21, 181\u2013185 (1985)","journal-title":"Inform. Process. Lett."},{"issue":"11","key":"83_CR4","doi-asserted-by":"crossref","first-page":"1015","DOI":"10.1109\/32.256850","volume":"19","author":"A. Arora","year":"1993","unstructured":"Arora A., Gouda M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Software Eng. 19(11), 1015\u20131027 (1993)","journal-title":"IEEE Trans. Software Eng."},{"key":"83_CR5","doi-asserted-by":"crossref","unstructured":"Arora, A., Kulkarni, S.S.: Designing masking fault-tolerance via nonmasking fault-tolerance. IEEE Trans. Software Eng. 24(6), 435\u2013450 (1998) (A preliminary version appears in the Proceedings of the Fourteenth Symposium on Reliable Distributed Systems, Bad Neuenahr, 174\u2013185, 1995)","DOI":"10.1109\/32.689401"},{"key":"83_CR6","doi-asserted-by":"crossref","unstructured":"Attie, P.: Synthesis of large concurrent programs via pairwise composition. In: CONCUR\u201999: 10th International Conference on Concurrency Theory, pp. 130\u2013145 (1999)","DOI":"10.1007\/3-540-48320-9_11"},{"key":"83_CR7","doi-asserted-by":"crossref","unstructured":"Attie, P., Emerson, A.: Synthesis of concurrent programs for an atomic read\/write model of computation. ACM TOPLAS (a preliminary version of this paper appeared in PODC96) 23(2) (2001)","DOI":"10.1145\/383043.383044"},{"issue":"1","key":"83_CR8","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"P. Attie","year":"1998","unstructured":"Attie P., Emerson E.: Synthesis of concurrent systems with many similar processes. ACM Trans. Programming Lang. Syst. 20(1), 51\u2013115 (1998)","journal-title":"ACM Trans. Programming Lang. Syst."},{"key":"83_CR9","unstructured":"Attie, P.C., Arora, A., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS). (A preliminary version of this paper appeared in PODC 1998.) 26(1), 125 \u2013 185 (2004)"},{"key":"83_CR10","doi-asserted-by":"crossref","unstructured":"Bharadwaj, R., Heitmeyer, C.: Developing high assurance avionics systems with the SCR requirements method. In: Proceedings of the 19th Digital Avionics Systems Conference, Philadelphia, PA (2000)","DOI":"10.1109\/DASC.2000.886888"},{"key":"83_CR11","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Kulkarni, S.S.: Exploiting symbolic techniques in automated synthesis of distributed programs. In: IEEE International Conference on Distributed Computing Systems, pp. 3\u201310 (2007)","DOI":"10.21236\/ADA460390"},{"key":"83_CR12","doi-asserted-by":"crossref","unstructured":"Demirbas, M., Arora, A.: Convergence refinement. In: International Conference on Distributed Computing Systems, pp. 589\u2013597 (2002)","DOI":"10.1109\/ICDCS.2002.1022309"},{"key":"83_CR13","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11) (1974)","DOI":"10.1145\/361179.361202"},{"key":"83_CR14","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, USA (1990)"},{"key":"83_CR15","unstructured":"Duval, G., Julliand, J.: Modeling and verification of rubis micro-kernel with spin. The First SPIN Workshop (1995). Available at http:\/\/spinroot.com\/spin\/Workshops\/ws95\/papers.html"},{"key":"83_CR16","doi-asserted-by":"crossref","unstructured":"Ebnenasir, A.: Diconic addition of failsafe fault-tolerance. In: Proceedings of the 22nd IEEE\/ACM international conference on Automated Software Engineering, pp. 44\u201353 (2007)","DOI":"10.1145\/1321631.1321641"},{"key":"83_CR17","doi-asserted-by":"crossref","unstructured":"Ebnenasir, A., Kulkarni, S.S.: SAT-based synthesis of fault-tolerance. In: Fast Abstracts of International Conference on Dependable Systems and Networks, Palazzo dei Congressi, Florence, Italy (2004)","DOI":"10.1109\/DSN.2004.1311891"},{"key":"83_CR18","unstructured":"Ebnenasir, A., Kulkarni, S.S.: Efficient synthesis of failsafe fault-tolerant distributed programs. Tech. Rep. MSU-CSE-05-13, Computer Science and Engineering, Michigan State University, East Lansing, MI (2005)"},{"issue":"3","key":"83_CR19","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. Emerson","year":"1982","unstructured":"Emerson E., Clarke E.: Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2(3), 241\u2013266 (1982)","journal-title":"Sci Comput Program"},{"key":"83_CR20","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, MA, USA (1995)"},{"key":"83_CR21","doi-asserted-by":"crossref","unstructured":"G\u00e4rtner, F.C., Jhumka, A.: Automating the addition of failsafe fault-tolerance: Beyond fusion-closed specifications. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), Grenoble, France, LNCS 3253, pp. 183\u2013198 (2004)","DOI":"10.1007\/978-3-540-30206-3_14"},{"key":"83_CR22","unstructured":"Gouda, M., McGuire, T.: Correctness preserving transformations for network protocol compilers. Prepared for the Workshop on New Visions for Software Design and Productivity: Research and Applications (2001)"},{"issue":"4","key":"83_CR23","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund K., Pressburger T.: Model checking java programs using java pathfinder. Int. J. Software Tools Technol. Transf. (STTT) 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Software Tools Technol. Transf. (STTT)"},{"key":"83_CR24","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: From code to models. In: Proceedings of the Second International Conference on Application of Concurrency to System Design (ACSD\u201901), pp. 3\u201310 (2001)","DOI":"10.1109\/CSD.2001.981759"},{"key":"83_CR25","unstructured":"Joesang, A.: Security protocol verification using spin. The First SPIN Workshop (1995). Available at http:\/\/spinroot.com\/spin\/Workshops\/ws95\/papers.html"},{"key":"83_CR26","unstructured":"Kulkarni, S.S.: Component-based design of fault-tolerance. Ph.D. Thesis, Ohio State University (1999)"},{"key":"83_CR27","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 82\u201393 (2000)","DOI":"10.1007\/3-540-45352-0_9"},{"key":"83_CR28","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Arora, A., Chippada, A.: Polynomial time synthesis of Byzantine agreement. Symposium on Reliable Distributed Systems, pp. 130\u2013139 (2001)","DOI":"10.1109\/RELDIS.2001.969767"},{"key":"83_CR29","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Ebnenasir, A.: Enhancing the fault-tolerance of nonmasking programs. In: Proceedings of the 23rd International Conference on Distributed Computing Systems, pp. 441\u2013449 (2003)","DOI":"10.1109\/ICDCS.2003.1203494"},{"key":"83_CR30","unstructured":"Kulkarni, S.S., Ebnenasir, A.: A framework for automatic synthesis of fault-tolerance. Tech. Rep. MSU-CSE-03-16, Computer Science and Engineering, Michigan State University, East Lansing MI 48824, Michigan (2003)"},{"issue":"3","key":"83_CR31","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1109\/TDSC.2005.29","volume":"2","author":"S.S. Kulkarni","year":"2005","unstructured":"Kulkarni S.S., Ebnenasir A.: Complexity issues in automated synthesis of failsafe fault-tolerance. IEEE Trans. Depend. Secure Comput. 2(3), 201\u2013215 (2005)","journal-title":"IEEE Trans. Depend. Secure Comput."},{"issue":"3","key":"83_CR32","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"Lamport L., Shostak R., Pease M.: The Byzantine generals problem. ACM Trans. Programming Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Programming Lang. Syst."},{"issue":"5","key":"83_CR33","doi-asserted-by":"crossref","first-page":"766","DOI":"10.1006\/jpdc.2001.1828","volume":"62","author":"M. Nesterenko","year":"2002","unstructured":"Nesterenko M., Arora A.: Stabilization-preserving atomicity refinement. J. Parallel Distrib. Comput. 62(5), 766\u2013791 (2002)","journal-title":"J. Parallel Distrib. Comput."},{"key":"83_CR34","unstructured":"Varghese, G.: Self-stabilization by local checking and correction. Ph.D. Thesis, MIT\/LCS\/TR-583 (1993)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0083-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0083-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0083-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:24Z","timestamp":1559114724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0083-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7,31]]},"references-count":34,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["83"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0083-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7,31]]}}}