{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:34:18Z","timestamp":1740548058488,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231356"},{"type":"electronic","value":"9783540278634"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27863-4_29","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T16:51:50Z","timestamp":1284655910000},"page":"541-566","source":"Crossref","is-referenced-by-count":4,"title":["Modeling and Formal Verification of Production Automation Systems"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Ruf","sequence":"first","affiliation":[]},{"given":"Roland J.","family":"Weiss","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Rosenstiel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.E.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.Y. Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 1. Springer, Heidelberg (2001) (invited paper)"},{"issue":"1","key":"29_CR3","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1024437214071","volume":"23","author":"J. Ruf","year":"2003","unstructured":"Ruf, J., Kropf, T.: Symbolic verification and analysis of discrete timed systems. Journal on Formal Methods in System Design\u00a023(1), 67\u2013108 (2003)","journal-title":"Journal on Formal Methods in System Design"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/BFb0023727","volume-title":"Computer-Aided Verification","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 136\u2013145. Springer, Heidelberg (1991)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-48153-2_20","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Ruf","year":"1999","unstructured":"Ruf, J., Kropf, T.: Modeling and checking networks of communicating real-time process. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 256\u2013279. Springer, Heidelberg (1999)"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Ruf, J., Hoffmann, D.W., Kropf, T., Rosenstiel, W.: Simulation-guided property checking based on a multi-valued AR-automata. [30] 742\u2013748","DOI":"10.1109\/DATE.2001.915111"},{"issue":"1","key":"29_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Journal on Formal Methods in System Design\u00a019(1), 45\u201380 (2001)","journal-title":"Journal on Formal Methods in System Design"},{"key":"29_CR8","unstructured":"Object Management Group (OMG): Unified Modeling Language (UML), Version 1.5. Document formal\/03-03-01 (2003), http:\/\/www.omg.org"},{"key":"29_CR9","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1145\/581199.581240","volume-title":"15th International Symposium on Systems Synthesis","author":"J. Klose","year":"2002","unstructured":"Klose, J., Kropf, T., Ruf, J.: A visual approach to validating system level designs. In: 15th International Symposium on Systems Synthesis, pp. 186\u2013191. ACM Press, New York (2002)"},{"key":"29_CR10","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"21st International Conference on Software Engineering","author":"M.B. Dwyer","year":"1999","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering, pp. 411\u2013420. ACM Press, New York (1999)"},{"key":"29_CR11","unstructured":"Flake, S., M\u00fcller, W., Ruf, J.: Structured english for model checking specification. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. 3. GI\/ITG\/GMM Workshop, pp. 99\u2013108. VDE Verlag (2002)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-27863-4_13","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"S. Flake","year":"2004","unstructured":"Flake, S., M\u00fcller, W., Ruf, J.: A UML\/OCL extension for state-oriented temporal properties with applications for manufacturing 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. 206\u2013226. Springer, Heidelberg (2004)"},{"issue":"2","key":"29_CR13","first-page":"194","volume":"7","author":"W. Reif","year":"2001","unstructured":"Reif, W., Schellhorn, G., Vollmer, T., Ruf, J.: Correctness of efficient real-time model checking. Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification\u00a07(2), 194\u2013209 (2001)","journal-title":"Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification"},{"issue":"3","key":"29_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"29_CR15","first-page":"188","volume-title":"Proceedings of the 1993 IEEE\/ACM International Conference on CAD","author":"R.I. Bahar","year":"1993","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proceedings of the 1993 IEEE\/ACM International Conference on CAD, pp. 188\u2013191. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"29_CR16","volume-title":"System Design with SystemC","author":"T. Gr\u00f6tker","year":"2002","unstructured":"Gr\u00f6tker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"M\u00fcller, W., Ruf, J., Hoffmann, D.W., Gerlach, J., Kropf, T., Rosenstiel, W.: The simulation semantics of SystemC. [30] 64\u201370","DOI":"10.1109\/DATE.2001.915002"},{"key":"29_CR18","unstructured":"Ruf, J., Peranandam, P.M., Kropf, T., Rosenstiel, W.: Bounded property checking with symbolic simulation. In: Forum on Specification and Design Languages (2003)"},{"key":"29_CR19","unstructured":"Ruf, J.: RAVEN: Real-time analyzing and verification. Technical Report WSI 2000-3, University of T\u00fcbingen (2000)"},{"key":"29_CR20","series-title":"Amast Series In Computing","first-page":"129","volume-title":"Theories and Experiences for Real-Time System Development.","author":"S.V. Campos","year":"1994","unstructured":"Campos, S.V., Clarke, E.M.: Real-time symbolic model checking for discrete time models. In: Rus, T., Rattray, C. (eds.) Theories and Experiences for Real-Time System Development. Amast Series In Computing, vol.\u00a02, pp. 129\u2013145. World Scientific Publishing Corporation, Inc., River Edge (1994)"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Iwashita, H., Nakata, T.: Forward model checking techniques oriented to buggy designs. In: Proceedings of the 1997 IEEE\/ACM International Conference on CAD, pp. 400\u2013404. ACM and IEEE Computer Society Press (1997)","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"29_CR22","series-title":"Advances in Computers","volume-title":"Highly Dependable Software","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Zelkowitz, M. (ed.) Highly Dependable Software. Advances in Computers, vol.\u00a058, Academic Press, London (2003)"},{"key":"29_CR23","unstructured":"ISO\/IEC: Programming Languages \u2013 C++. 2. edn. Number 14882:2003 in JTC1\/SC22 \u2013 Programming languages, their environment and system software interfaces. International Organization for Standardization (2003)"},{"key":"29_CR24","unstructured":"VA Software Corporation, Open SystemC Initiative: Open SystemC Initiative (2004), www.systemc.org"},{"issue":"2","key":"29_CR25","first-page":"120","volume":"9","author":"A. Krebs","year":"2003","unstructured":"Krebs, A., Ruf, J.: Optimized temporal logic compilation. Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification\u00a09(2), 120\u2013137 (2003)","journal-title":"Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification"},{"key":"29_CR26","unstructured":"Flake, S., M\u00fcller, W.: A UML profile for MFERT. Technical Report 4, C-LAB Paderborn (2002)"},{"key":"29_CR27","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III: Verification and Control","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems III: Verification and Control, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"29_CR28","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT)\u00a01(1-2), 123\u2013133 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"29_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/3-540-63166-6_46","volume-title":"Computer Aided Verification","author":"S.V.A. Campos","year":"1997","unstructured":"Campos, S.V.A., Clarke, E.M., Minea, M.: The Verus tool: A quantitative approach to the formal verification of real-time systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 452\u2013455. Springer, Heidelberg (1997)"},{"volume-title":"Design, Automation and Test in Europe, DATE 2001","year":"2001","key":"29_CR30","unstructured":"Nebel, W., Jerraya, A. (eds.): Design, Automation and Test in Europe, DATE 2001. IEEE Press, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Integration of Software Specification Techniques for Applications in Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27863-4_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T21:49:56Z","timestamp":1740520196000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27863-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231356","9783540278634"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27863-4_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}