{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T04:02:30Z","timestamp":1750046550857,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319486277"},{"type":"electronic","value":"9783319486284"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-48628-4_12","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T12:45:31Z","timestamp":1488372331000},"page":"285-310","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From ProCoS to Space and Mental Models\u2013A Survey of Combining Formal and Semi-formal Methods"],"prefix":"10.1007","author":[{"given":"Bettina","family":"Buth","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"12_CR1","unstructured":"Buth, B.: Formal and Semi-Formal Methods for the Analysis of Industrial Control Systems. Bremen University (2002)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Buth, B.: Analysing mode confusion: an approach using FDR2. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, vol. 3219, pp. 101\u2013114. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-30138-7_9"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Buth, B., Peleska, J.: Formal methods for large-scale industrial applications \u2013 deadlock and livelock analysis for the international space station. In: Tutorial Material for the Advanced Summer School in Formal Methods and Applications, Beijing, China, October 1999","DOI":"10.1007\/3-540-48092-7_16"},{"key":"12_CR4","unstructured":"Buth, B., Cardell-Oliver, R., Peleska, J.: Combining tools for the verification of fault-tolerant systems. In: Berghammer, R., Buth, B., Peleska, J. (eds.) Tools for Software Development and Verification. BISS Monographs, vol. 1. Shaker-Verlag (1996) (in print)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Buth, B., Kouvaras, M., Peleska, J., Shi, H.: Deadlock analysis for a fault-tolerant system. In: Johnson, M. (ed.) Algebraic Methodology and Software Technology. Proceedings of AMAST\u201997. LNCS, vol. 1349 , pp. 60\u201375. Springer, December 1997","DOI":"10.1007\/BFb0000463"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Buth, B., Peleska, J., Shi, H.: Combining methods for the analysis of a fault-tolerant system. In: Haeberer, A.M. (ed.) Algebraic Methodology and Software Technology, Proceedings of AMAST\u201998. LNCS, vol. 1548, pp. 124\u2013139. Springer, January 1999","DOI":"10.1007\/3-540-49253-4_11"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Buth, B., Peleska, J., Shi, H.: Combining methods for the analysis of a fault-tolerant system. In: Proceedings of Quality Week \u201999, May 1999. (CDrom)","DOI":"10.1007\/3-540-49253-4_11"},{"key":"12_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569760","volume-title":"Specification and Proof in Real-Time CSP","author":"J Davies","year":"1993","unstructured":"Davies, J.: Specification and Proof in Real-Time CSP. Cambridge University Press, New York (1993)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Dill, D.: The mur $$\\phi $$ verification system. In: Alur, R., Henzinger, T. (eds.) Computer Aided Verification, CAV\u201996. LNCS, vol. 1102. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61474-5_86"},{"key":"12_CR10","unstructured":"Formal Systems (Europe) Lts. FDR2 User Manual, FDR 2.97 edition. http:\/\/www.fsel.com\/documentation\/fdr2\/html\/fdr2manual.html"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"12_CR12","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Red Series. Prentice-Hall International, Englewood Cliffs (1985)"},{"key":"12_CR13","unstructured":"inmos ltd. occam 2 Reference Manual. Series in Computer Science. Prentice Hall International (1988)"},{"issue":"3","key":"12_CR14","doi-asserted-by":"publisher","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. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR15","unstructured":"Leveson, N.G., Palmer, E.: Designing automation to reduce operator errors. In: Proceedings of the IEEE Systems, Man, and Cybernetics Conference (1997)"},{"key":"12_CR16","unstructured":"Levevson, N.G., Pinnel, L.D., Sandys, S.D., Koga, S., Rees, J.D.: Analyzing software specifications for mode confusion potential. In: Johnson, C.W. (ed.) Proceedings of a Workshop on Human Error and System Development, Glasgow, Scotland, Glasgow Accident Analysis Group, Technical Report GAAG-TR-97-2, pp.\u00a0132\u2013146, March 1997"},{"key":"12_CR17","unstructured":"L\u00fcttgen, G., Carre\u00f1o, V.: Analyzing mode confusion via model checking. Technical Report NASA\/CR-1999-209332, ICASE Report No.\u00a099-18, ICASE - NASA Langley Research Center, May 1999. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.95.5171&rep=rep1&type=pdf"},{"key":"12_CR18","unstructured":"Miller, S.P., Potts, J.N.: Detecting mode confusion through formal modeling and analysis. Technical Report NASA\/CR-1999-208971, NASA Langley Research Center, January 1999. https:\/\/shemesh.larc.nasa.gov\/fm\/papers\/Miller-99-cr208971-Mode-Confusion.pdf"},{"key":"12_CR19","unstructured":"Palmer, E.: Oops, it didn\u2019t arm. A case study of two automation surprises. In: Jensen, R.S., Rakovan, L.A. (eds.) Proceedings of the 8th International Symposium on Aviation Psychology, Columbus, OH, The Aviation Psychology Department of Aerospace Engineering, Ohio State University, pp. 227\u2013232, April 1995."},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-48092-7_16","volume-title":"Correct System Design - Recent Insights and Advances","author":"J Peleska","year":"1999","unstructured":"Peleska, J., Buth, B.: Formal methods for the international space station iss. In: Olderog, E.R., Steffen, B. (eds.) Correct System Design - Recent Insights and Advances. Lecture Notes in Computer Science, vol. 1710, pp. 363\u2013389. Springer, Heidelberg (1999)"},{"key":"12_CR21","unstructured":"Peleska, J., Shi, H., Kouvaras, M.: Combining methods for the analysis of a fault-tolerant system. In: Proceedings of the 1999 Pacific Rim International Symposium on Dependable Computing (PRDC 1999) (1999) (Submitted)"},{"key":"12_CR22","unstructured":"Rushby, J., Crow, J., Palmer, E.: An automated method to detect potential mode confusions. In: 18th AIAA\/IEEE Digital Avionics Systems Conference, St. Louis (MO) (1999)"},{"key":"12_CR23","unstructured":"Roscoe, A.W.: Model-checking CSP. In: A Classical Mind, Eassys in Honour of C.A.R. Hoare. Prentice-Hall International (1997)"},{"key":"12_CR24","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Upper Saddle River (1997)"},{"key":"12_CR25","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Upper Saddle River (1998)"},{"key":"12_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems, 1st edn. Springer, New York (2010)","edition":"1"},{"key":"12_CR27","unstructured":"Rushby, J.: Using model checking to help discover mode confusion and other automation surprises. In: Proceedings of the 3rd Workshop on Human Error, Safety, and System Development (HESSD\u201999), Liege, Belgium (1999)"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. In: Reliability Engineering and System Safety (2002)","DOI":"10.1016\/S0951-8320(01)00092-8"},{"key":"12_CR29","volume-title":"Handbook of Human Factors and Ergonomics","author":"NB Sarter","year":"1997","unstructured":"Sarter, N.B., Woods, D.D., Billings, C.E.: Automation surprises. In: Salvendy, G. (ed.) Handbook of Human Factors and Ergonomics. Wiley, New York (1997)"},{"key":"12_CR30","unstructured":"Schr\u00f6nen, M.: Methodology for the Development of Microprocessor-Based Safety-Critical Systems. Monographs of the Bremen Institute of Safet Systems\u00a08, Bremen University (1998). Shaker Verlag, Aachen"},{"key":"12_CR31","volume-title":"Concurrent and Real-Time Systems: The CSP Approach","author":"S Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real-Time Systems: The CSP Approach. Wiley, New York (1999)"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Twele, L., Schlingloff, H., Szczerbicka, H.: Performability analysis of an avionics-interface. In: Proceedings of IEEE Conference on Systems, Man and Cybernetics, San Diego, N.J., pp. 499\u2013504 (1998)","DOI":"10.1109\/ICSMC.1998.725461"},{"key":"12_CR33","unstructured":"University of Oxford. FDR3 User Manual, FDR 3.4 edition. https:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/index.html"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T22:19:47Z","timestamp":1750025987000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_12","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"type":"print","value":"1860-0131"},{"type":"electronic","value":"2197-6597"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"2 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}