{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:51:09Z","timestamp":1725565869189},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231356"},{"type":"electronic","value":"9783540278634"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27863-4_13","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T16:51:50Z","timestamp":1284655910000},"page":"206-226","source":"Crossref","is-referenced-by-count":6,"title":["Specification and Formal Verification of Temporal Properties of Production Automation Systems"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Flake","sequence":"first","affiliation":[]},{"given":"Wolfgang","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Ulrich","family":"Pape","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Ruf","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Baar, T., H\u00e4hnle, R.: An Integrated Metamodel for OCL Types. In: France, R., Rumpe, B., Bruel, J.-M., Moreira, A., Whittle, J., Ober, I. (eds.) OOPSLA 2000 Workshop Refactoring the UML: In Search of the Core, Minneapolis, MN, USA (2000)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-45923-5_14","volume-title":"Fundamental Approaches to Software Engineering","author":"J.C. Bradfield","year":"2002","unstructured":"Bradfield, J.C., K\u00fcster Filipe, J., Stevens, P.: Enriching OCL Using Observational Mu-Calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, pp. 203\u2013217. Springer, Heidelberg (2002)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BFb0054174","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"U. Brockmeyer","year":"1998","unstructured":"Brockmeyer, U., Wittich, G.: Tamagotchis Need Not Die \u2014 Verification of STATEMATE Designs. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 217\u2013231. Springer, Heidelberg (1998)"},{"key":"13_CR4","first-page":"38","volume-title":"Joint 9th European Software Engineering Conference (ESEC) and 11th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE-11)","author":"S. Burmester","year":"2003","unstructured":"Burmester, S., Flake, S., Giese, H., Sch\u00e4fer, W., Tichy, M.: Towards the Compositional Verification of Real-Time UML Designs. In: Inverardi, P., Paakki, J. (eds.) Joint 9th European Software Engineering Conference (ESEC) and 11th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE-11), Helsinki, Finland, September 2003, pp. 38\u201347. ACM Press, New York (2003)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-45614-7_22","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"M.V. Cengarle","year":"2002","unstructured":"Cengarle, M.V., Knapp, A.: Towards OCL\/RT. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 389\u2013408. Springer, Heidelberg (2002)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Cheng, A.: Petri Nets, Traces, and Local Model Checking. In: Algebraic Methodology and Software Technology, pp. 322\u2013337 (1995)","DOI":"10.1007\/3-540-60043-4_62"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Object Modeling with the OCL","year":"2002","unstructured":"Clark, A., Warmer, J. (eds.): Object Modeling with the OCL. LNCS, vol.\u00a02263. Springer, Heidelberg (2002)"},{"key":"13_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR9","first-page":"151","volume-title":"Unified Modeling Language: Systems Analysis, Design, and Development Issues","author":"S. Conrad","year":"2001","unstructured":"Conrad, S., Turowski, K.: Temporal OCL: Meeting Specifications Demands for Business Components. In: Siau, K., Halpin, T. (eds.) Unified Modeling Language: Systems Analysis, Design, and Development Issues, pp. 151\u2013165. IDEA Group Publishing, USA (2001)"},{"issue":"1","key":"13_CR10","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. Formal Methods in System Design\u00a019(1), 45\u201380 (2001)","journal-title":"Formal Methods in System Design"},{"key":"13_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60860-5","volume-title":"Fertigungslenkung: Planung und Steuerung des Ablaufs der diskreten Fertigung","author":"W. Dangelmaier","year":"1997","unstructured":"Dangelmaier, W., Warnecke, H.-J.: Fertigungslenkung: Planung und Steuerung des Ablaufs der diskreten Fertigung. Springer, Heidelberg (1997)"},{"key":"13_CR12","volume-title":"Modell der Fertigungssteuerung","author":"W. Dangelmaier","year":"1993","unstructured":"Dangelmaier, W., Wiedenmann, H.: Modell der Fertigungssteuerung, 1st edn. Beuth Verlag GmbH, Berlin (1993)","edition":"1"},{"key":"13_CR13","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-0-387-35520-7_16","volume-title":"Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000)","author":"D. Distefano","year":"2000","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: On a Temporal Logic for Object-Based Systems. In: Smith, S., Talcott, C. (eds.) Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000), Stanford, CA, USA, September 2000, pp. 305\u2013326. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"21st International Conference on Software Engineering (ICSE 1999)","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 (ICSE 1999), Los Angeles, CA, USA, May 1999, pp. 411\u2013420. ACM Press, New York (1999)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/3-540-63010-4_11","volume-title":"Transformation-Based Reactive Systems Development","author":"K. Feyerabend","year":"1997","unstructured":"Feyerabend, K., Josko, B.: A Visual Formalism for Real Time Requirement Specifications. In: Rus, T., Bertr\u00e1n, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol.\u00a01231, pp. 156\u2013168. Springer, Heidelberg (1997)"},{"key":"13_CR16","first-page":"580","volume-title":"7th IASTED International Conference on Software Engineering and Applications (SEA 2003)","author":"S. Flake","year":"2003","unstructured":"Flake, S.: Modeling and Verification of Manufacturing Systems: A Domain-Specific Formalization of UML. In: Hamza, M. (ed.) 7th IASTED International Conference on Software Engineering and Applications (SEA 2003), Los Angeles, CA, USA, November 2003, pp. 580\u2013586. ACTA Press, Calgary (2003)"},{"key":"13_CR17","unstructured":"Flake, S.: UML-Based Specification of State-oriented Real-time Properties. PhD thesis, Faculty of Computer Science, Electrical Engineering and Mathematics, Paderborn University, Shaker Verlag, Aachen, Germany (December 2003)"},{"key":"13_CR18","series-title":"Australian Computer Science Communications","first-page":"73","volume-title":"27th Australasian Computer Science Conference (ACSC 2004)","author":"S. Flake","year":"2004","unstructured":"Flake, S.: Towards the Completion of the Formal Semantics of OCL 2.0. In: Estivill-Castro, V. (ed.) 27th Australasian Computer Science Conference (ACSC 2004), Dunedin, New Zealand, January 2004. Australian Computer Science Communications, vol.\u00a026, pp. 73\u201382. Australian Computer Science Society, Sydney (2004)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Flake, S., M\u00fcller, W.: An OCL Extension for Real-Time Constraints. In: Clark and Warmer [7], pp. 150\u2013171","DOI":"10.1007\/3-540-45669-4_8"},{"key":"13_CR20","volume-title":"35th Hawaii International Conference on System Sciences (HICSS-35)","author":"S. Flake","year":"2002","unstructured":"Flake, S., M\u00fcller, W.: Specification of Real-Time Properties for UML Models. In: Sprague Jr., R. (ed.) 35th Hawaii International Conference on System Sciences (HICSS-35), Big Island, HI, USA, January 2002, IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"13_CR21","first-page":"595","volume-title":"The 2003 International Conference on Software Engineering Research and Practice (SERP 2003)","author":"S. Flake","year":"2003","unstructured":"Flake, S., M\u00fcller, W.: Expressing Property Specification Patterns with OCL. In: The 2003 International Conference on Software Engineering Research and Practice (SERP 2003), Las Vegas, NV, USA, June 2003, pp. 595\u2013601. CSREA Press, Las Vegas (2003)"},{"issue":"3","key":"13_CR22","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10270-003-0026-x","volume":"2","author":"S. Flake","year":"2003","unstructured":"Flake, S., M\u00fcller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Software and Systems Modeling (SoSyM)\u00a02(3), 164\u2013186 (2003)","journal-title":"Software and Systems Modeling (SoSyM)"},{"key":"13_CR23","first-page":"251","volume-title":"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen","author":"S. Flake","year":"2000","unstructured":"Flake, S., M\u00fcller, W., Ruf, J.: Structured English for Model Checking Specification. In: Waldschmidt, K., Grimm, C. (eds.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Frankfurt\/M., Germany, February 2000, pp. 251\u2013262. VDE Verlag, Berlin (2000)"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Holt, A., Klein, E.: A Semantically-Derived Subset of English for Hardware Verification. In: 37th Annual Meeting of the Association for Computational Linguistics (ACL 1999), University of Maryland, College Park, MD, USA, June 1999, pp. 451\u2013456 (1999)","DOI":"10.3115\/1034678.1034747"},{"key":"13_CR25","unstructured":"Ivner, A., H\u00f6gstr\u00f6m, J., Johnston, S., Knox, D., Rivett, P.: Response to the UML2.0 OCL RfP, Version 1.6 (Submitters: Boldsoft, Rational, IONA, Adaptive Ltd., et al.). OMG Document ad\/03-01-07 (January 2003), ftp:\/\/ftp.omg.org\/pub\/-docs\/ad\/03-01-07.pdf"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-48234-2_7","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"W. Janssen","year":"1999","unstructured":"Janssen, W., Mateescu, R., Mauw, S., Fennema, P., van der Stappen, P.: Model Checking for Managers. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 92\u2013107. Springer, Heidelberg (1999)"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Springer International Journal of Software Tools for Technology Transfer 1(1+2) (1997)","DOI":"10.1007\/s100090050010"},{"key":"13_CR28","unstructured":"OMG, Object Management Group. UML 2.0 OCL Final Adopted Specification. OMG Document ptc\/03-10-14 (October 2003), ftp:\/\/ftp.omg.org\/pub\/docs\/ptc\/-03-10-14.pdf"},{"key":"13_CR29","unstructured":"OMG, Object Management Group. Unified Modeling Language 1.5 Specification. OMG Document formal\/03-03-01 (March 2003), ftp:\/\/ftp.omg.org\/pub\/-docs\/formal\/03-03-01.pdf"},{"key":"13_CR30","unstructured":"Ramakrishnan, S., McGregor, J.: Extending OCL to Support Temporal Operators. In: 21st International Conference on Software Engineering (ICSE 1999), Workshop on Testing Distributed Component-Based Systems, Los Angeles, CA, USA (May 1999)"},{"key":"13_CR31","unstructured":"Richters, M.: A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universit\u00e4t Bremen, Bremen, Germany, Logos Verlag, Berlin, BISS Monographs, No. 14 (2002)"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Richters, M., Gogolla, M.: OCL: Syntax, Semantics, and Tools. In: Clark and Warmer [7], pp. 42\u201368","DOI":"10.1007\/3-540-45669-4_4"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Rosenblum, D.: Formal Methods and Testing: Why State-Of-The-Art is not State- Of-The-Practise. In: ISSTA 1996\/FMSP 1996 Panel Summary. ACM SIGSOFT Software Engineering Notes 21(4) (July 1996)","DOI":"10.1145\/232069.232086"},{"key":"13_CR34","unstructured":"Roubtsova, E.E., van Katwijk, J., Toetenel, W., de Rooij, R.C.: Real-Time Systems: Specification of Properties in UML. In: 7th Annual Conference of the Advanced School for Computing and Imaging (ASCI 2001), Het Heijderbos, Heijen, The Netherlands, May\/June 2001, pp. 188\u2013195 (2001)"},{"key":"13_CR35","unstructured":"Ruf, J.: Techniken zur Modellierung und Verifikation von Echtzeitsystemen. PhD thesis, Universit\u00e4t Karlsruhe, Karlsruhe, Germany (March 2000) (in German)"},{"issue":"1","key":"13_CR36","first-page":"89","volume":"7","author":"J. Ruf","year":"2001","unstructured":"Ruf, J.: RAVEN: Real-Time Analyzing and Verification Environment. Journal on Universal Computer Science (J.UCS)\u00a07(1), 89\u2013104 (2001)","journal-title":"Journal on Universal Computer Science (J.UCS)"},{"key":"13_CR37","first-page":"146","volume-title":"Correct Hardware Design and Verification Methods (CHARME 1997), 9th IFIP WG 10.5 Advanced Research Working Conference","author":"J. Ruf","year":"1997","unstructured":"Ruf, J., Kropf, T.: Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In: Cerny, E., Probst, D. (eds.) Correct Hardware Design and Verification Methods (CHARME 1997), 9th IFIP WG 10.5 Advanced Research Working Conference, Montreal, Canada, October 1997, pp. 146\u2013166. Chapman and Hall, Boca Raton (1997)"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","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 Systems. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 265\u2013279. Springer, Heidelberg (1999)"},{"key":"13_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-27863-4_29","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"J. Ruf","year":"2004","unstructured":"Ruf, J., Kropf, T., Weiss, R.: Modeling and Formal Verification of Production Automation 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. 541\u2013566. Springer, Heidelberg (2004)"},{"key":"13_CR40","unstructured":"Schneider, U.: Ein formales Modell und eine Klassifikation f\u00fcr die Fertigungssteuerung \u2013 Ein Beitrag zur Systematisierung der Fertigungssteuerung. PhD thesis, Heinz Nixdorf Institut, HNI-Verlagsschriftenreihe, Band 16, Paderborn, Germany (1996) (in German)"},{"key":"13_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/3-540-45441-1_29","volume-title":"\u00abUML\u00bb 2001 \u2013 The Unified Modeling Language. Modeling Languages, Concepts, and Tools","author":"S. Sendall","year":"2001","unstructured":"Sendall, S., Strohmeier, A.: Specifying Concurrent System Behavior and Timing Constraints Using OCL and UML. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol.\u00a02185, pp. 391\u2013405. Springer, Heidelberg (2001)"},{"key":"13_CR42","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1999)"},{"key":"13_CR43","series-title":"Object Technology Series","volume-title":"The Object Constraint Language \u2013 Getting Your Models Ready for MDA","author":"J. Warmer","year":"2003","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language \u2013 Getting Your Models Ready for MDA, 2nd edn. Object Technology Series. Addison-Wesley, Reading (2003)","edition":"2"},{"key":"13_CR44","unstructured":"Westk\u00e4mper, E., H\u00f6pf, M., Schaeffer, C.: Holonic Manufacturing Systems (HMS) \u2013 Test Case 5. In: Proceedings of Holonic Manufacturing Systems, Lake Tahoe, CA, USA (February 1994)"},{"key":"13_CR45","unstructured":"Ziemann, P., Gogolla, M.: An Extension of OCL with Temporal Logic. In: J\u00fcrjens, J., Cengarle, M., Fernandez, E., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML \u2013 Proceedings of the UML 2002 Workshop, Technische Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik, Munich, Germany, pp. 53\u201362 (2002)"}],"container-title":["Lecture Notes in Computer Science","Integration of Software Specification Techniques for Applications in Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27863-4_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:36Z","timestamp":1605759876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27863-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231356","9783540278634"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27863-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}