{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T16:36:21Z","timestamp":1649090181924},"reference-count":168,"publisher":"Elsevier","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1016\/b978-0-12-408089-8.00004-5","type":"book-chapter","created":{"date-parts":[[2013,8,17]],"date-time":"2013-08-17T04:45:20Z","timestamp":1376714720000},"page":"119-205","source":"Crossref","is-referenced-by-count":6,"title":["Model-Driven Engineering of Reliable Fault-Tolerant Systems\u2014A State-of-the-Art Survey"],"prefix":"10.1016","author":[{"given":"Vidar","family":"Sl\u00e5tten","sequence":"first","affiliation":[]},{"given":"Peter","family":"Herrmann","sequence":"additional","affiliation":[]},{"given":"Frank Alexander","family":"Kraemer","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0005","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1234741.1234767","article-title":"A looming fault tolerance software crisis?","volume":"32","author":"Romanovsky","year":"2007","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0010","unstructured":"Canada-U.S. Power System Outage Task Force, Interim Report: Causes of the August 14th Black Out in the United States and in Canada, November 2003."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0015","series-title":"Software Engineering of FaultTolerant Systems","article-title":"An introduction to software engineering and fault tolerance","volume":"vol. 19","author":"Pelliccione","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0020","unstructured":"G.N. Rodrigues, A Model Driven Approach for Software Reliability Prediction, Ph.D. Thesis, University College London, March 2008."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0025","series-title":"Proceedings of the 26th International Conference on Software Engineering (ICSE\u201904)","first-page":"30","article-title":"A model driven approach for software systems reliability","author":"Rodrigues","year":"2004"},{"issue":"6","key":"10.1016\/B978-0-12-408089-8.00004-5_b0030","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1016\/j.jvlc.2006.10.002","article-title":"A survey of approaches for the visual model-driven development of next generation software-intensive systems","volume":"17","author":"Giese","year":"2006","journal-title":"J. Visual Lang. Comput."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0035","series-title":"Model Driven Architecture D Foundations and Applications","first-page":"419","article-title":"MDA-based methodologies: an analytical survey","volume":"vol. 5095","author":"Asadi","year":"2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0040","unstructured":"Object Management Group. MDA Website (online) , 2011 (cited December 2011)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0045","series-title":"Model-Based Engineering of Embedded Real-Time Systems","first-page":"77","article-title":"Semantics of UML models for dynamic behavior","volume":"vol. 6100","author":"Lund","year":"2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0050","series-title":"Scientific Engineering of Distributed Java Applications","first-page":"78","article-title":"A survey of software development approaches addressing dependability","volume":"vol. 3409","author":"Mustafiz","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0055","series-title":"Software Engineering for Self-Adaptive Systems","first-page":"1","article-title":"Software engineering for self-adaptive systems: a research roadmap","volume":"vol. 5525","author":"Cheng","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0060","series-title":"Conceptual Modeling: Foundations and Applications","first-page":"363","article-title":"On non-functional requirements in software engineering","volume":"vol. 5600","author":"Chung","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0065","unstructured":"H. Muccini, A. Romanovsky, Architecting fault tolerant systems, Technical Report CS-TR-1051, University of Newcastle upon Tyne, Newcastle upon Tyne, England, September 2007. "},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0070","unstructured":"Object Management Group (OMG), Unified Modeling Language: Superstructure, Version 2.4.1. , August 2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0075","unstructured":"ITU-T, Recommendation Z.100: Specification and Description Language (SDL). , November 2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0080","unstructured":"ITU-T, Recommendation Z.120: Message Sequence Charts (MSC). , February 2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0085","series-title":"Real-Time Object-Oriented Modeling","author":"Selic","year":"1994"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0090","series-title":"Domain-Specific Modeling: Enabling Full Code Generation","author":"Kelly","year":"2008"},{"issue":"10","key":"10.1016\/B978-0-12-408089-8.00004-5_b0095","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1145\/383845.383858","article-title":"Getting started with AspectJ","volume":"44","author":"Kiczales","year":"2001","journal-title":"Commun. ACM"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0100","series-title":"Transactions on Aspect-Oriented Software Development VI","first-page":"191","article-title":"MATA: a unified approach for composing UML aspect models based on graph transformation","author":"Whittle","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0105","series-title":"Abstract state machines: a method for high-level system design and analysis","author":"Borger","year":"2003"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0110","series-title":"Model Driven Engineering Languages and Systems","first-page":"42","article-title":"Improving the definition of UML","volume":"vol. 4199","author":"O\u2019Keefe","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0115","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MS.2010.145","article-title":"Point\/Counterpoint","volume":"27","author":"Woods","year":"2010","journal-title":"IEEE Software"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0120","unstructured":"Object Management Group (OMG), Semantics of a Foundational Subset for Executable UML Models (fUML), Version 1.0. , February 2011"},{"issue":"2","key":"10.1016\/B978-0-12-408089-8.00004-5_b0125","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","article-title":"The existence of refinement mappings","volume":"82","author":"Abadi","year":"1991","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0130","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/TDSC.2004.2","article-title":"Basic concepts and taxonomy of dependable and secure computing","volume":"1","author":"Avizienis","year":"2004","journal-title":"IEEE Trans. Depend. Secure Comput."},{"issue":"6","key":"10.1016\/B978-0-12-408089-8.00004-5_b0135","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1145\/390016.808467","article-title":"System structure for software fault tolerance","volume":"10","author":"Randell","year":"1975","journal-title":"SIGPLAN Not."},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0140","first-page":"41","article-title":"CHAOS: the dollar drain of IT project failures","volume":"2","author":"Johnson","year":"1995","journal-title":"vol. 2 of Appl. Dev. Trends"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0145","series-title":"Spectrum, IEEE","first-page":"42","article-title":"Why software fails","author":"Charette","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0150","series-title":"Proceedings of the 11th international conference on Model Driven Engineering Languages and Systems, MoDELS \u201908","first-page":"736","article-title":"Adding dependability analysis capabilities to the MARTE profile","author":"Bernardi","year":"2008"},{"issue":"6","key":"10.1016\/B978-0-12-408089-8.00004-5_b0155","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1109\/71.774912","article-title":"The timed asynchronous distributed system model","volume":"10","author":"Cristian","year":"1999","journal-title":"IEEE Trans. Parall. Distr. Syst."},{"issue":"2","key":"10.1016\/B978-0-12-408089-8.00004-5_b0160","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1348246.1348249","article-title":"A survey of linguistic structures for application-level fault tolerance","volume":"40","author":"Florio","year":"2008","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0165","series-title":"CurrentTrends in Concurrency. Overviews and Tutorials","first-page":"510","article-title":"Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends","volume":"vol. 224","author":"Pnueli","year":"1986"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0170","series-title":"Fault Tolerant Systems","author":"Koren","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0175","series-title":"Fault Tolerance: Principles and Practice","author":"Anderson","year":"1981"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0180","series-title":"Proceedings of the 2007 OTM Confederated international conference on On the Move to Meaningful Internet Systems: CoopIS, DOA, ODBASE, GADA, and IS\u2014Volume Part I, OTM\u201907","first-page":"505","article-title":"A survey of fault tolerant CORBA systems","author":"Fahad","year":"2007"},{"issue":"4","key":"10.1016\/B978-0-12-408089-8.00004-5_b0185","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1145\/98163.98167","article-title":"Implementing fault-tolerant services using the state machine approach: a tutorial","volume":"22","author":"Schneider","year":"1990","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0190","series-title":"Advances in Distributed Systems","article-title":"Consensus in asynchronous distributed systems: a concise guided tour","volume":"vol. 1752","author":"Guerraoui","year":"2000"},{"issue":"12","key":"10.1016\/B978-0-12-408089-8.00004-5_b0195","doi-asserted-by":"crossref","first-page":"1491","DOI":"10.1109\/TSE.1985.231893","article-title":"The N-version approach to fault-tolerant software","volume":"11","author":"Avizienis","year":"1985","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0200","series-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier","year":"2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0205","unstructured":"Object Management Group (OMG), Object Constraint Language (OCL), Version 2.3.1. , January 2012"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0210","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0215","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0220","series-title":"Proceedings of the Fifth International Conference on Software Language Engineering-SLE2012","first-page":"83","article-title":"Temporal constraint support for ocl","volume":"vol. 7745","author":"Kanso","year":"2013"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0225","series-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS \u201977","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"issue":"3","key":"10.1016\/B978-0-12-408089-8.00004-5_b0230","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0235","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0240","series-title":"Proceedings of the Seventh ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, POPL \u201980","first-page":"174","article-title":"\u201cSometime\u201d is sometimes \u201cnot never\u201d: on the temporal logic of programs","author":"Lamport","year":"1980"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0245","series-title":"Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201999)","first-page":"54","article-title":"Model checking TLA+ specifications","volume":"vol. 1703","author":"Yu","year":"1999"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0250","series-title":"Specifying Systems","author":"Lamport","year":"2002"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0255","series-title":"Spin model checker, the: primer and reference manual","author":"Holzmann","year":"2003"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0260","series-title":"Proceedings of the Fourth Annual Symposium on Logic in computer science","first-page":"353","article-title":"Compositional model checking","author":"Clarke","year":"1989"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0265","series-title":"Practical Model-Based Testing: A Tools Approach","author":"Utting","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0270","series-title":"Model-Driven Testing: Using the UML Testing Profile","author":"Baker","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0275","series-title":"Automated Theorem Proving in Software Engineering","author":"Schumann","year":"2001"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0280","series-title":"10th International SPIN Workshop on Model Checking of Software, Portland, Oregon","first-page":"121","article-title":"What went wrong: explaining counterexamples","author":"Groce","year":"2003"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0285","series-title":"POPL \u201903: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"97","article-title":"From symptom to cause: localizing errors in counterexample traces","author":"Ball","year":"2003"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0290","series-title":"Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics","first-page":"1157","article-title":"Distributed computing: models and methods","author":"Lamport","year":"1990"},{"issue":"2","key":"10.1016\/B978-0-12-408089-8.00004-5_b0295","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/3149.214121","article-title":"Impossibility of distributed consensus with one faulty process","volume":"32","author":"Fischer","year":"1985","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/B978-0-12-408089-8.00004-5_b0300","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/226643.226647","article-title":"Unreliable failure detectors for reliable distributed systems","volume":"43","author":"Chandra","year":"1996","journal-title":"Journal of the ACM"},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0305","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/1052796.1052806","article-title":"A short introduction to failure detectors for asynchronous distributed systems","volume":"36","author":"Raynal","year":"2005","journal-title":"SIGACT News"},{"issue":"4","key":"10.1016\/B978-0-12-408089-8.00004-5_b0310","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1109\/MIC.2008.75","article-title":"Convenience over correctness","volume":"12","author":"Vinoski","year":"2008","journal-title":"Internet Comput. IEEE"},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0315","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/2080.357392","article-title":"Implementing remote procedure calls","volume":"2","author":"Birrell","year":"1984","journal-title":"ACM Trans. Comput. Syst."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0320","unstructured":"J. Spolsky, The Law of Leaky Abstractions. , November 2002 (cited 18.02.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0325","series-title":"Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006)","first-page":"77","article-title":"Architecting fault-tolerant component-based systems: from requirements to testing","volume":"168","author":"Bucchiarone","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0330","series-title":"Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-13","first-page":"111","article-title":"CHARMY: an extensible tool for architectural analysis","author":"Inverardi","year":"2005"},{"issue":"3","key":"10.1016\/B978-0-12-408089-8.00004-5_b0335","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.2008.104","article-title":"Charmy: a framework for designing and verifying architectural specifications","volume":"35","author":"Pelliccione","year":"2009","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0340","series-title":"Proceedings of the 2006 International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, SCESM \u201906","first-page":"21","article-title":"A scenario based notation for specifying temporal properties","author":"Autili","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0345","series-title":"Component-Based Software Engineering","first-page":"267","article-title":"TeStor: deriving test sequences from model-based specifications","volume":"vol. 3489","author":"Pelliccione","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0350","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/ICSE.2002.1007967","article-title":"ArchJava: connecting software architecture to implementation","author":"Aldrich","year":"2002","journal-title":"Software Engineering, ICSE 2002. Proceedings of the 24rd International Conference on IEEE"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0355","unstructured":"Charmy project (online). , February 2006 (cited 19.02.13)"},{"issue":"12","key":"10.1016\/B978-0-12-408089-8.00004-5_b0360","doi-asserted-by":"crossref","first-page":"2068","DOI":"10.1016\/j.jss.2009.06.057","article-title":"Tool support for the rapid composition, analysis and implementation of reactive services","volume":"82","author":"Kraemer","year":"2009","journal-title":"J. Syst. Softw."},{"issue":"2009.1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0365","first-page":"135","article-title":"Compositional service engineering with arctis","volume":"105","author":"Kraemer","year":"2009","journal-title":"Telektronikk"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0370","series-title":"Formal Techniques for Distributed Systems","first-page":"17","article-title":"Reactive semantics for distributed UML activities","volume":"vol. 6117","author":"Kraemer","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0375","series-title":"Proceedings of the Eighth International Symposium on Distributed Objects and Applications (DOA), 2006, Montpellier, France","first-page":"1613","article-title":"Aligning UML 2.0 state machines and temporal logic for the efficient execution of services","volume":"vol. 4276","author":"Kraemer","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0380","series-title":"Formal Techniques for Distributed Systems","first-page":"304","article-title":"Contracts for multi-instance UML activities","volume":"vol. 6722","author":"Sl\u00e5tten","year":"2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0385","series-title":"Proceedings of the 10th International Conference on Generative Programming and Component Engineering (GPCE\u201911)","article-title":"Towards automatic generation of formal specifications to validate and verify reliable distributed systems\u2014a method exemplified by an industrial case study","author":"Sl\u00e5tten","year":"2011"},{"issue":"4","key":"10.1016\/B978-0-12-408089-8.00004-5_b0390","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1145\/357401.357402","article-title":"End-to-end arguments in system design","volume":"2","author":"Saltzer","year":"1984","journal-title":"ACM Trans. Comput. Syst."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0395","series-title":"Proceedings of the Second International Workshop on Software Engineering for Resilient Systems (SERENE 2010)","first-page":"2","article-title":"Towards a model-driven method for reliable applications: from ideal to realistic transmission semantics","author":"Sl\u00e5tten","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0400","series-title":"Proceedings of the 12th International Conference on Model Driven Engineering Languages and Systems (MoDELS)","first-page":"571","article-title":"Automated encapsulation of UML activities for incremental development and verification","author":"Kraemer","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0405","unstructured":"Developer\u2014Bitreactive. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0410","series-title":"The B-book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0415","unstructured":"A. Iliasov, E. Troubitsyna, L. Laibinis, A. Romanovsky, K. Varpaaniemi, D. Ilic, T. Latvala, Developing mode-rich satellite software by refinement in event-b, Science of Computer Programming. "},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0420","unstructured":"Deploy project\u2014industrial deployment of system engineering methods providing high dependability and productivity. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0425","unstructured":"UML-B\u2014Event-B. , December 2012 (cited 21.03.13.)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0430","unstructured":"D23 ProB-B\u2014Event-B. , January 2010 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0435","series-title":"Contemporary Computing","first-page":"625","article-title":"Verification of liveness properties in distributed systems","volume":"vol. 40","author":"Yadav","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0440","series-title":"Formal Methods and Software Engineering","first-page":"456","article-title":"Reasoning about liveness properties in Event-B","volume":"vol. 6991","author":"Hoang","year":"2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0445","unstructured":"Code Generation Activity\u2014Event-B. , December 2012 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0450","series-title":"Second International Workshop on Software Engineering for Resilient Systems (SERENE), London, United Kingdom","article-title":"On fault tolerance reuse during renement","author":"Lopatkin","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0455","series-title":"Abstract State Machines, Alloy, B and Z","first-page":"174","article-title":"Supporting reuse in Event B development: modularisation approach","volume":"vol. 5977","author":"Iliasov","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0460","unstructured":"Event-B.org. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0465","series-title":"FM\u201999\u2014Formal Methods","first-page":"712","article-title":"Meteor: a successful application of B in a large project","volume":"vol. 1708","author":"Behm","year":"1999"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0470","series-title":"Model-Based Engineering of Embedded Real-Time Systems","first-page":"309","article-title":"Fujaba4Eclipse real-time tool suite","volume":"vol. 6100","author":"Priesterjahn","year":"2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0475","series-title":"Model Driven Architecture","first-page":"900","article-title":"Model-driven development of reconfigurable mechatronic systems with MECHATRONIC UML","volume":"vol. 3599","author":"Burmester","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0480","series-title":"Model Driven Architecture\u2014Foundations and Applications","first-page":"25","article-title":"Model-driven architecture for hard real-time systems: from platform independent models to code","author":"Burmester","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0485","unstructured":"S. Burmester, H. Giese, M. Hirsch, Syntax and semantics of hybrid components, Technical Report TR-RI-05-264, University of Paderborn, October 2005."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0490","unstructured":"CAMeL-View. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0495","series-title":"Selected Papers From the Sixth International Workshop on Theory and Application of Graph Transformations, TAGT\u201998","first-page":"296","article-title":"Story diagrams: a new graph rewrite language based on the unified modeling language and java","author":"Fischer","year":"2000"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0500","unstructured":"UP4ALL Inc\u2014uppaal.com. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0505","unstructured":"UPPAAL. , October 2012 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0510","unstructured":"P. Dibble, The real-time specification for Java (JSR-001). , July 2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0515","series-title":"Postproc. of the Fourth Workshop on Object-oriented Modeling of Embedded Real-Time Systems (OMER 4), Paderborn, Germany","article-title":"Component story diagrams: a transformation language for component structures in mechatronic systems","author":"Tichy","year":"2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0520","unstructured":"H. Giese, S. Burmester, Real-time statecharts semantics, Technical Report TR-RI-03-239, University of Paderborn, June 2003."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0525","series-title":"Companion of the 30th international conference on Software engineering, ICSE Companion \u201908","first-page":"973","article-title":"Safety of component-based systems: analysis and improvement using Fujaba4Eclipse","author":"Tichy","year":"2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0530","series-title":"Proceedings of the Doctoral Symposium of the 14th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE)","first-page":"13","article-title":"Pattern-based Synthesis of Fault-Tolerant Embedded Systems","author":"Tichy","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0535","unstructured":"B. Becker, H. Giese, S. Hildebrandt, A. Seibel, Fujabas future in the MDA jungle, Technical Report TUD-FI08-09, Technische Universit\u00e4t Dresden, Fakult\u00e4t Informatik, September 2008."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0540","unstructured":"J. Johannes, Letting EMF tools talk to Fujaba through adapters, Technical Report TUD-FI08-09, Technische Universit\u00e4t Dresden, Fakult\u00e4t Informatik, September 2008."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0545","series-title":"Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering ICSE \u201910\u2014Volume 2","first-page":"267","article-title":"Legacy component integration by the Fujaba real-time tool suite","author":"Henkler","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0550","unstructured":"Home\u2014Railcab. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0555","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s11390-009-9219-2","article-title":"Architecting fault tolerance with exception handling: verification and validation","volume":"24","author":"Brito","year":"2009","journal-title":"J. Comput. Sci. Technol."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0560","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1002\/spe.632","article-title":"Exception handling in the development of dependable component-based systems","volume":"35","author":"Rubira","year":"2005","journal-title":"Softw. Pract. Exper."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0565","series-title":"Dependable Computing","first-page":"61","article-title":"A Method for modeling and testing exceptions in component-based software development","volume":"vol. 3747","author":"da Brito","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0570","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/LADC.2011.23","article-title":"Validation of exception handling in the development of dependable component-based software systems","author":"Ferreira","year":"2011","journal-title":"2011 Fifth Latin-American Symposium on Dependable Computing (LADC)"},{"issue":"8","key":"10.1016\/B978-0-12-408089-8.00004-5_b0575","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Commun. ACM"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0580","series-title":"FM 2005: Formal Methods","first-page":"631","article-title":"Combining CSP and B for specification and property verification","volume":"vol. 3582","author":"Butler","year":"2005"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0585","series-title":"Proceedings of the Eighth Brazilian Workshop on Test and Fault Tolerance (WTF 2007), Bel\u00e9m, Par\u00e1, Brazil","first-page":"99","article-title":"Uso de modelos da uml em testes de componentes (eng.: using uml models for component test)","author":"Perez","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0590","unstructured":"Object Management Group (OMG), MOF\/XMI Mapping, Version 2.4.1. , August 2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0595","unstructured":"Download\u2014ProB Documentation. , March 2013 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0600","unstructured":"ProBLicence\u2014ProB Documentation. , April 2012 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0605","unstructured":"Formal Mind\u2014Science for Systems Engineering. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0610","series-title":"Proceedings of the Sixth International Conference on Aspect-Oriented Software Development (AOSD), Industry Track, Vancouver, Canada","article-title":"The Motorola WEAVR: model weaving in a large industrial context","author":"Cottenier","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0615","unstructured":"IBM, Bm Rational Tau User Guide. , June 2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0620","unstructured":"Welcome, TO ETSI\u2019S OFFICIAL TTCN-3 HOMEPAGE. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0625","unstructured":"Telecommunication standardization sector of ITU (ITU-T), ITU-T Recommendation Z.109 \u2013 SDL-2000 combined with UML. , June 2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0630","unstructured":"ITU-T, Recommendation Z.100: Specification and Description Language (SDL), Annex F. , November 2000"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0635","unstructured":"IBM\u2014Rational Tau\u2014Features and benefits. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0640","unstructured":"Rational DOORS. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0645","unstructured":"T. Cottenier, A. van den Berg, T. Elrad. Motorola WEAVR. , October 2006 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0650","unstructured":"Motorola WEAVR\u2014LICENSES. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0655","series-title":"Third IEEE International Conference on Self-Adaptive and Self-Organizing Systems, SASO \u201909","first-page":"206","article-title":"MOCAS: a state-based component model for self-adaptation","author":"Ballagny","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0660","series-title":"Fourth European Congress EMBEDDED REAL TIME SOFTWARE (ERTS)","article-title":"Introducing simulation and model animation in the MDE Topcased toolkit","author":"Combemale","year":"2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0665","series-title":"Proceedings of the 14th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe \u201909","first-page":"207","article-title":"Formal verification of AADL specifications in the topcased environment","author":"Berthomieu","year":"2009"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0670","series-title":"Modeling Foundations and Applications","first-page":"3","article-title":"Contracts for model execution verification","volume":"vol. 6698","author":"Cariou","year":"2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0675","unstructured":"Topcased\u2014Home. , February 2013 (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0680","unstructured":"MOCASEngine\/MOCAS For TopCased Plugin at SourceForge.net. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0685","unstructured":"MOCASEngine. (cited 21.03.13)"},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0690","first-page":"17","article-title":"rCOS: a formal model-driven engineering method for component-based software","volume":"6","author":"Ke","year":"2012","journal-title":"Front. Comput. Sci. China"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0695","series-title":"15th IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW), IEEE 2012","first-page":"37","article-title":"Component based design of fault tolerant devices in cyber physical system","author":"Xu","year":"2012"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0700","series-title":"Proceedings of the Eighth Australian workshop on Safety critical Systems and Software\u2014Volume 33, SCS \u201903","first-page":"37","article-title":"A new component concept for fault trees","author":"Kaiser","year":"2003"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0705","series-title":"Unifying Theories of Programming, vol. 14,","author":"Hoare","year":"1998"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0710","series-title":"Leveraging Applications of Formal Methods, Verification, and Validation,","first-page":"609","article-title":"AutoPA: automatic prototyping from requirements","volume":"vol. 6415","author":"Li","year":"2010"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0715","unstructured":"Formal Systems (Europe) Ltd\u2014Software. (cited 21.03.13)"},{"issue":"10","key":"10.1016\/B978-0-12-408089-8.00004-5_b0720","doi-asserted-by":"crossref","first-page":"879","DOI":"10.1016\/j.scico.2010.02.005","article-title":"Robustness testing for software components","volume":"75","author":"Lei","year":"2010","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0725","unstructured":"The rCOS Modeler. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0730","unstructured":"MDT\/UML2\u2014Eclipsepedia. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0735","series-title":"The Common Component Modeling Example","first-page":"116","article-title":"Modeling with relational calculus of object and component systems\u2014rCOS","volume":"vol. 5153","author":"Chen","year":"2008"},{"issue":"4","key":"10.1016\/B978-0-12-408089-8.00004-5_b0740","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1016\/j.scico.2008.08.003","article-title":"Refinement and verification in component-based model-driven design","volume":"74","author":"Chen","year":"2009","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0745","unstructured":"Common Component Modeling Example. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0750","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.entcs.2010.08.050","article-title":"Design and verification of a trustable medical system","volume":"266","author":"Xiong","year":"2010","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0755","series-title":"11th IEEE International Conference on Engineering of Complex Computer Systems, 2006. ICECCS 2006","article-title":"Reactive component based service-oriented design-a case study","author":"Liu","year":"2006"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0760","series-title":"IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing, ISORC \u201909","first-page":"47","article-title":"Fault-tolerance for component-based systems\u2014an automated middleware specialization approach","author":"Tambe","year":"2009"},{"issue":"2","key":"10.1016\/B978-0-12-408089-8.00004-5_b0765","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/S0141-9331(02)00096-0","article-title":"Total quality of service provisioning in middleware and applications","volume":"27","author":"Wang","year":"2003","journal-title":"Microprocess. Microsyst."},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0770","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.scico.2008.05.005","article-title":"Model driven middleware: a new paradigm for developing distributed real-time and embedded systems","volume":"73","author":"Gokhale","year":"2008","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0775","unstructured":"Object Management Group (OMG), Common Object Request Broker Architecture (CORBA) Specification, Version 3.1.1. , August 2011"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0780","unstructured":"Object Management Group (OMG), Asynchronous Method Invocation for CORBA Component Model (AMI4CCM), Version 1.0\u2014Beta 2. , December 2012"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0785","unstructured":"Home\u2014The ACE ORB. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0790","unstructured":"CoSMIC Project Page. (cited 21.03.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0795","unstructured":"Component-Integated ACE ORB (CIAO). (cited 21.3.13)"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0800","series-title":"Architecting Dependable Systems IV","first-page":"163","article-title":"Model-centric development of highly available software systems","volume":"vol. 4615","author":"Buskens","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0805","unstructured":"Aurora Management Workbench. (cited 21.03.13)."},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0810","unstructured":"EMF Diff\/Merge. (cited 21.03.13)"},{"issue":"12","key":"10.1016\/B978-0-12-408089-8.00004-5_b0815","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/163298.163303","article-title":"The process group approach to reliable distributed computing","volume":"36","author":"Birman","year":"1993","journal-title":"Commun. ACM"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0820","unstructured":"Object Management Group (OMG), UML Profile for Modeling Quality of Service and Fault Tolerance Characteristics and Mechanisms (QFTP), Version 1.1. , April 2008"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0825","series-title":"10th IEEE Symposium on High Assurance Systems Engineering, 2007, HASE \u201907","first-page":"275","article-title":"Pattern-based modeling and analysis of failsafe fault-tolerance in uml","author":"Ebnenasir","year":"2007"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0830","series-title":"Architecting Dependable Systems II","first-page":"394","article-title":"Reliability support for the model driven architecture","volume":"vol. 3069","author":"Rodrigues","year":"2004"},{"issue":"1","key":"10.1016\/B978-0-12-408089-8.00004-5_b0835","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1327452.1327492","article-title":"Mapreduce: simplified data processing on large clusters","volume":"51","author":"Dean","year":"2008","journal-title":"Commun. ACM"},{"key":"10.1016\/B978-0-12-408089-8.00004-5_b0840","unstructured":"Google Scholar. (cited 21.03.13)"}],"container-title":["Advances in Computers"],"original-title":[],"deposited":{"date-parts":[[2018,10,13]],"date-time":"2018-10-13T17:56:36Z","timestamp":1539453396000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780124080898000045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":168,"URL":"http:\/\/dx.doi.org\/10.1016\/b978-0-12-408089-8.00004-5","relation":{},"ISSN":["0065-2458"],"issn-type":[{"value":"0065-2458","type":"print"}],"published":{"date-parts":[[2013]]}}}