{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:00Z","timestamp":1725559200027},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540258131"},{"type":"electronic","value":"9783540322658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11423348_19","type":"book-chapter","created":{"date-parts":[[2010,7,14]],"date-time":"2010-07-14T06:36:01Z","timestamp":1279089361000},"page":"293-320","source":"Crossref","is-referenced-by-count":3,"title":["Applied Formal Methods \u2013 From CSP to Executable Hybrid Specifications"],"prefix":"10.1007","author":[{"given":"Jan","family":"Peleska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-60117-1_6","volume-title":"Mathematics of Program Construction","author":"A.E. Abdallah","year":"1995","unstructured":"Abdallah, A.E.: Derivation of Parallel Algorithms: From Functional Specifications to csp Processes. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 67\u201396. Springer, Heidelberg (1995)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-45449-7_2","volume-title":"Embedded Software","author":"R. Alur","year":"2001","unstructured":"Alur, R., Dang, T., Esposito, J., Fierro, R., Hur, Y., Ivan\u010di\u0107, F., Kumar, V., Lee, I., Mishra, P., Pappas, G., Sokolsky, O.: Hierarchical hybrid modeling of embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 14\u201331. Springer, Heidelberg (2001)"},{"key":"19_CR3","unstructured":"Amthor, P.: Structural Decomposition of Hybrid Systems \u2013 Test Automation for Hybrid Reactive Systems. In: Monographs of the Bremen Institute of Safe Systems (BISS), October 1999, vol.\u00a013, University of Bremen (1999)"},{"key":"19_CR4","series-title":"Texts and monographs in computer science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of sequential and concurrent programs","author":"K.R. Apt","year":"1991","unstructured":"Apt, K.R., Olderog, E.-R.: Verification of sequential and concurrent programs. Texts and monographs in computer science, p. 441. Springer, Heidelberg (1991)"},{"key":"19_CR5","unstructured":"Berkenk\u00f6tter, K., Bisanz, S., Hannemann, U., Peleska, J.: HybridUML Profile for UML 2.0. In: SVERTS Workshop at the \u2329\u2329 UML \u232a\u232a 2003 Conference (October 2003), \n                    \n                      http:\/\/www-verimag.imag.fr\/EVENTS\/2003\/SVERTS\/"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-27863-4_10","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"K. Berkenk\u00f6tter","year":"2004","unstructured":"Berkenk\u00f6tter, K., Bisanz, S., Hannemann, U., Peleska, J.: Executable HybridUML and its application to train control systems. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 145\u2013173. Springer, Heidelberg (2004)"},{"key":"19_CR7","unstructured":"Buth, B., Cardell-Oliver, R., Peleska, J.: Combining tools for the verification of fault-tolerant systems. In: Buth, B., Berghammer, R., Peleska, J. (eds.) Tools for System Development and Verification, 1998. Monographs of the Bremen Institute of Safe Systems, vol.\u00a01, pp. 41\u201369. Shaker (1998)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0000463","volume-title":"Algebraic Methodology and Software Technology","author":"B. Buth","year":"1997","unstructured":"Buth, B., Kouvaras, M., Peleska, J., Shi, H.: Deadlock analysis for a fault-tolerant system. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol.\u00a01349, pp. 60\u201375. Springer, Heidelberg (1997)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/3-540-49253-4_11","volume-title":"Algebraic Methodology and Software Technology","author":"B. Buth","year":"1998","unstructured":"Buth, B., Peleska, J., Shi, H.: Combining methods for the livelock analysis of a fault-tolerant system. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 124\u2013139. Springer, Heidelberg (1998)"},{"key":"19_CR10","unstructured":"Brinksma, E., Tretmans, J.: Testing transition systems: An annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M. (eds.) Proceedings of Summer School MOVEP\u20192k Modelling and Verification of Parallel Processes, Nantes, July 2000, pp. 44\u201350 (2000)"},{"issue":"3","key":"19_CR11","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"SE-4","author":"T.S. Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering\u00a0SE-4(3), 178\u2013186 (1978)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1984","unstructured":"De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theoretical Computer Science\u00a034, 83\u2013133 (1984)","journal-title":"Theoretical Computer Science"},{"key":"19_CR13","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/978-0-387-35271-8_31","volume-title":"Formal Description Techniques and Protocol Specification, Verification, and Testing (FORTE\/PSTV 1997)","author":"C. Fischer","year":"1997","unstructured":"Fischer, C., Smith, G.: Combining CSP and Object-Z: Finite trace or infinite trace semantics? In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) Formal Description Techniques and Protocol Specification, Verification, and Testing (FORTE\/PSTV 1997), 1997, pp. 503\u2013518. Chapman & Hall, Boca Raton (1997)"},{"key":"19_CR14","unstructured":"Formal Systems (Europe) Ltd. Failures\u2013Divergence Refinement \u2013 FDR2 User Manual (2001), \n                    \n                      http:\/\/www.formal.demon.co.uk\/FDR2.html."},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/LICS.1996.561342","volume-title":"Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS)","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS), pp. 278\u2013292. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/JPROC.2002.805825","volume":"91","author":"T..A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE\u00a091, 84\u201399 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"19_CR17","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"19_CR18","unstructured":"Haxthausen, A.E., Peleska, J.: Generation of executable railway control components from domain-specific descriptions. In: Tarnai, G., Schnieder, E. (eds.) Formal Methods for Railway Operation and Control Systems: Proceedings of Symposium FORMS, Budapest, May 2003, pp. 83\u201390. L\u2019Harmattan Hongrie (2003)"},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01786251","volume":"2","author":"H. Jifeng","year":"1987","unstructured":"Jifeng, H., Hoare, C.A.R.: Algebraic specification and proof of a distributed recovery algorithm. Distributed Computing\u00a02, 1\u201312 (1987)","journal-title":"Distributed Computing"},{"key":"19_CR20","series-title":"International Series in Computer Science","first-page":"171","volume-title":"A Classical Mind, Essays in Honour of C.A.R.\u00a0Hoare","author":"H. Jifeng","year":"1994","unstructured":"Jifeng, H.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind, Essays in Honour of C.A.R.\u00a0Hoare. International Series in Computer Science, pp. 171\u2013189. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"19_CR21","unstructured":"Kendelbacher, D.: Architekturkonzept und Designaspekte einer signaltechnisch nichtsicheren Kommunikationsplattform f\u00fcr sicherheitsrelevante Bahnanwendungen. PhD thesis, University of Bremen, Department of Mathematics and Computer Science, Available under (2004), \n                    \n                      http:\/\/elib.suub.uni-bremen.de\/publications\/dissertations\/E-Diss835_dis_50b.pdf."},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/11423348_17","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"R. Lazic","year":"2005","unstructured":"Lazic, R., Newcomb, T., Roscoe, B.: On model checking data-independent systems with arrays with whole-array operations. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol.\u00a03525, pp. 275\u2013291. Springer, Heidelberg (2005)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Transactions on Programming Languages and Systems\u00a04(3) (1982)","DOI":"10.1145\/357172.357176"},{"key":"19_CR24","unstructured":"Meyer, O.: Structural Decomposition of Timed-CSP and its Application in Real-Time Testing. PhD thesis, TZI Center for Computing Technologies, University of Bremen, Germany (2001)"},{"key":"19_CR25","unstructured":"Meyer, O., Tsiolakis, A., Berkhahn, S.-O., Kruse, J., Martinen, D.: Automated testing of aircraft controller modules. In: Proceeding s of the 5th International Conference on Software Testing ICSTEST, D\u00fcsseldorf, April 2004, SQS (2004), Extended abstract and slides available under,\n                    \n                      http:\/\/www.informatik.uni-bremen.de\/~tsio\/papers\/"},{"key":"19_CR26","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","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. LNCS, vol.\u00a01710, pp. 363\u2013389. Springer, Heidelberg (1999)"},{"issue":"1","key":"19_CR27","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF02259751","volume":"5","author":"J. Peleska","year":"1991","unstructured":"Peleska, J.: Design and verification of fault tolerant systems with csp. Distributed Computing\u00a05(1), 95\u2013106 (1991)","journal-title":"Distributed Computing"},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-60973-3_79","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"J. Peleska","year":"1996","unstructured":"Peleska, J.: Test automation for safety-critical systems: Industrial application and future developments. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 39\u201359. Springer, Heidelberg (1996)"},{"key":"19_CR29","unstructured":"Peleska, J.: Formal Methods and the Development of Dependable Systems. Bericht Nr. 9612. Christian-Albrechts-Universit\u00e4t Kiel, Institut f\u00fcr Informatik und praktische Mathematik (1997), Habilitation thesis, available under, \n                    \n                      http:\/\/www.informatik.uni-bremen.de\/agbs\/jp"},{"key":"19_CR30","unstructured":"Peleska, J.: Formal methods for test automation - hard real-time testing of controllers for the airbus aircraft family. In: Proc. of the Sixth Biennial World Conference on Integrated Design & Process Technology (IDPT2002), June 2002. Society for Design and Process Science (2002), Available under, \n                    \n                      http:\/\/www.informatik.uni-bremen.de\/agbs\/jp\/papers\n                    \n                    \n                  ."},{"key":"19_CR31","unstructured":"Peleska, J.: Automated testsuites for modern aircraft controllers. In: Drechsler, R. (ed.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Aachen, pp. 1\u201310. Shaker (2003)"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/3-540-60973-3_106","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"J. Peleska","year":"1996","unstructured":"Peleska, J., Siegel, M.: From Testing Theory to Test Driver Implementation. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 538\u2013556. Springer, Heidelberg (1996)"},{"key":"19_CR33","first-page":"53","volume":"19","author":"J. Peleska","year":"1997","unstructured":"Peleska, J., Siegel, M.: Test automation of safety-critical reactive systems. South African Computer Jounal\u00a019, 53\u201377 (1997)","journal-title":"South African Computer Jounal"},{"key":"19_CR34","unstructured":"Peleska, J., Tsiolakis, A.: Automated Integration Testing for Avionics Systems. In: Proceedings of the 3rd ICSTEST \u2013 International Conference on Software Testing (April 2002), Extended abstract and slides available under, \n                    \n                      http:\/\/www.informatik.uni-bremen.de\/agbs\/jp"},{"key":"19_CR35","unstructured":"Ravn, A.P.: Design of embedded real-time computing systems. Technical Report ID-TR 1995-170, ID\/DTU, Lyngby, Denmark, dr. techn. dissertation (October 1995)"},{"key":"19_CR36","volume-title":"The Unified Modeling Language \u2013 Reference Manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language \u2013 Reference Manual. Addison-Wesley, Reading (1999)"},{"key":"19_CR37","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"19_CR38","volume-title":"Concurrent and Real-time Systems \u2013 The CSP Approach","author":"S. Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-time Systems \u2013 The CSP Approach. Wiley and Sons Ltd., Chichester (2000)"},{"key":"19_CR39","unstructured":"Schlingloff, H., Meyer, O., H\u00fclsing, T.: Correctness Analysis of an Embedded Controller. In: Proceedings of DASIA (Data Systems in Aerospace) 1999 Conference, Lisbon, Portugal, vol.\u00a0ESA SP-447 (1999)"},{"issue":"1-2","key":"19_CR40","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0304-3975(99)00134-6","volume":"254","author":"J. Springintveld","year":"2001","unstructured":"Springintveld, J., Vaandrager, F.W., D\u2019Argenio, P.R.: Testing timed automata. Theoretical Computer Science\u00a0254(1-2), 225\u2013257 (2001)","journal-title":"Theoretical Computer Science"},{"key":"19_CR41","first-page":"372","volume-title":"The Twenty-Eighth Annual International Symposium on Fault-Tolerant Computing","author":"G. Urban","year":"1998","unstructured":"Urban, G., Kolinowitz, H.-J., Peleska, J.: A survivable avionics system for space applications. In: The Twenty-Eighth Annual International Symposium on Fault-Tolerant Computing, Munich, Germany, June 23-25, vol.\u00a0FTCS-28, pp. 372\u2013379. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"19_CR42","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-57318-6_23","volume-title":"Hybrid Systems","author":"A.. Chaochen Zhou","year":"1993","unstructured":"Chaochen Zhou, A., Ravn, P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Hybrid Systems, pp. 36\u201359. The Computer Society of the IEEE, Los Alamitos (1993) Extended abstract"}],"container-title":["Lecture Notes in Computer Science","Communicating Sequential Processes. The First 25 Years"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11423348_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:04:56Z","timestamp":1619507096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11423348_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540258131","9783540322658"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/11423348_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}