乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,28]],"date-time":"2025-01-28T05:11:26Z","timestamp":1738041086652,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781264"},{"type":"electronic","value":"9783540781271"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78127-1_5","type":"book-chapter","created":{"date-parts":[[2008,2,7]],"date-time":"2008-02-07T12:59:40Z","timestamp":1202389180000},"page":"72-86","source":"Crossref","is-referenced-by-count":1,"title":["Synthesis of Monitors for Real-Time Analysis of Reactive Systems"],"prefix":"10.1007","author":[{"given":"Mikhail","family":"Auguston","sequence":"first","affiliation":[]},{"given":"Mark","family":"Trakhtenbrot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Auguston, M.: Program Behavior Model Based on Event Grammar and its Application for Debugging Automation. In: 2nd Int\u2019l Workshop on Automated and Algorithmic Debugging, AADEBUG 1995, pp. 277\u2013291 (May 1995)"},{"key":"5_CR2","unstructured":"Auguston, M., Gates, A., Lujan, M.: Defining a Program Behavior Model for Dynamic Analyzers. In: 9th International Conference on Software Engineering and Knowledge Engineering, SEKE 1997, pp. 257\u2013262 (June 1997)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Avrunin, G.S., Corbett, J.C., Dwyer, M.B.: Property Specification Patterns for Finite-State Verification. In: 2nd Workshop on Formal Methods in Software Practice, pp. 7\u201315 (March 1998)","DOI":"10.1145\/298595.298598"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., et al.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-48257-1_6","volume-title":"Applied Formal Methods - FM-Trends 98","author":"K. Bogdanov","year":"1999","unstructured":"Bogdanov, K., Holcombe, M., Singh, H.: Automated Test Set Generation for Statecharts. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 107\u2013121. Springer, Heidelberg (1999)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1109\/LICS.1994.316045","volume-title":"Proceedings of the 9th IEEE Symposium Logic in Computer Science (LICS 1994)","author":"E.S. Chang","year":"1994","unstructured":"Chang, E.S., Manna, Z., Pnueli, A.: Compositional Verification of Real-time Systems. In: Proceedings of the 9th IEEE Symposium Logic in Computer Science (LICS 1994), pp. 458\u2013465. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.R.: A Language Framework for Expressing Checkable Properties of Dynamic Software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 205\u2013223. Springer, Heidelberg (2000)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/3-540-65193-4_29","volume-title":"Lectures on Embedded Systems","author":"B.P. Douglass","year":"1998","unstructured":"Douglass, B.P., Harel, D., Trakhtenbrot, M.: Statecharts in Use: Structured Analysis and Object-Orientation. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol.\u00a01494, pp. 368\u2013394. Springer, Heidelberg (1998)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., et al.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47884-1_1","volume-title":"Integrated Formal Methods","author":"E. Gery","year":"2002","unstructured":"Gery, E., Harel, D., Palatchi, E.: Rhapsody: A Complete Lifecycle Model-Based Development System. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 1\u201310. Springer, Heidelberg (2002)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming\u00a08, 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-540-27863-4_19","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"D. Harel","year":"2004","unstructured":"Harel, D., Kugler, H.: The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML). In: Ehrig, H., et al. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 325\u2013354. Springer, Heidelberg (2004)"},{"issue":"4","key":"5_CR13","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., et al.: STATEMATE: A Working Environment for the Development of Complex Reactive Systems. IEEE Trans. on Software Engineering\u00a016(4), 403\u2013414 (1990)","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"4","key":"5_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE Semantics of Statecharts. ACM Trans. on Software Engineering Method\u00a05(4), 293\u2013333 (1996)","journal-title":"ACM Trans. on Software Engineering Method"},{"key":"5_CR15","unstructured":"Harel, D., et al.: On the Formal Semantics of Statecharts. In: Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, NY, pp. 54\u201364 (1987)"},{"key":"5_CR16","volume-title":"Modeling Reactive Systems with Statecharts: The STATEMATE Approach","author":"D. Harel","year":"1998","unstructured":"Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York (1998)"},{"key":"5_CR17","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1991)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-54415-1_49","volume-title":"Theoretical Aspects of Computer Software","author":"A. Pnueli","year":"1991","unstructured":"Pnueli, A., Shalev, M.: What is in a Step: On the Semantics of Statecharts. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 244\u2013264. Springer, Heidelberg (1991)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Richardson, D., Leif Aha, S., Owen O\u2019Malley, T.: Specification-based Test Oracles for Reactive Systems. In: Proc. Fourteens Intl. Conf. on Software Engineering, Melbourne, pp. 105\u2013118 (1992)","DOI":"10.1109\/ICSE.1992.753494"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/10722167_45","volume-title":"Computer Aided Verification","author":"T. Bienm\u00fcller","year":"2000","unstructured":"Bienm\u00fcller, T., Damm, W., Wittke, H.: The STATEMATE Verification Environment - Making It Real. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 561\u2013567. Springer, Heidelberg (2000)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Strichman, O., Goldring, R.: The \u2019Logic Assurance (LA)\u2019 System - A Tool for Testing and Controlling Real-Time Systems. In: Proc. 8th Israeli Conference on Computer Systems and Software Engineering, pp. 47\u201356 (1997)","DOI":"10.1109\/ICCSSE.1997.599875"},{"key":"5_CR22","unstructured":"Thanne, M., Yerushalmi, R.: Experience with an Advanced Design Flow with OSEK Compliant Code Generation for Automotive ECU\u2019s. Dedicated Systems Magazine, Special Issue on Development Methodologies & Tools, 6\u201311 (2001)"},{"key":"5_CR23","unstructured":"Wind River Systems, Inc. BetterState, http:\/\/www.windriver.com\/products\/betterstate\/index.html"}],"container-title":["Lecture Notes in Computer Science","Pillars of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78127-1_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,27]],"date-time":"2025-01-27T04:34:25Z","timestamp":1737952465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78127-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781264","9783540781271"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78127-1_5","relation":{},"subject":[]}}