{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T20:40:07Z","timestamp":1760820007001},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540654933"},{"type":"electronic","value":"9783540492139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49213-5_8","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T07:03:39Z","timestamp":1197183819000},"page":"186-238","source":"Crossref","is-referenced-by-count":37,"title":["A Compositional Real-time Semantics of STATEMATE Designs"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Josko","sequence":"additional","affiliation":[]},{"given":"Hardi","family":"Hungar","sequence":"additional","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,5,21]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness","author":"M. Abadi","year":"1990","unstructured":"Mart\u00edn Abadi and Leslie Lamport. Composing specifications. In Jaco W. de Bakker, Willem-Paul de Roever, and Grzegorz Rozenberg, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, Lecture Notes in Computer Science430, pages 1\u201341. Springer-Verlag, 1990."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9):1270\u20131282, September 1991.","DOI":"10.1109\/5.97297"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"U. Brockmeyer and G. Wittich. Tamagotchis need not die-verification of Statemate designs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998), 1998. (To appear).","DOI":"10.1007\/BFb0054174"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking. In ACM\/IEEE Design Automation Conference, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 428\u2013439, June 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"8_CR6","unstructured":"Werner Damm and Johannes Helbig. Linking visual formalisms: A compositional proof system for statecharts based on symbolic timing diagrams. In Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET\u201994), pages 337\u2013356, 1994."},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot. STATEMATE: A working environment for the development od complex reactive systems. IEEE Transactions on Software Engineering, 16:403\u2013414, 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR8","unstructured":"D. Harel and A. Naamad. The STATEMATE semantics of statecharts. Technical Report CS95-31, The Weizmann Institute of Science, Rehovot, 1995."},{"key":"8_CR9","unstructured":"D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman. On the formal semantics of statecharts. In Proceeding IEEE Symposium on Logic in Computer Science, pages 54\u201364, 1987."},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1145\/42411.42414","volume":"31","author":"D. Harel","year":"1988","unstructured":"David Harel. On visual formalism. CACM, 31:514\u2013530, 1988.","journal-title":"CACM"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"David Harel and Amir Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series F13, pages 477\u2013498. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1"},{"key":"8_CR13","unstructured":"David Harel and Michal Politi. Modeling reactive systems with statecharts: The statemate approach. Technical report, 1996."},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(92)90053-I","volume":"101","author":"J.J.M. Hooman","year":"1992","unstructured":"J.J.M. Hooman, S. Ramesh, and W.P. de Roever. A compositional axiomatization of statecharts. TCS, 101:289\u2013335, 1992.","journal-title":"TCS"},{"key":"8_CR15","unstructured":"Bernhard Josko. Modular Specification and Verification of Reactive Systems. Habilitationsschrift, Universit\u00e4t Oldenburg, 1993."},{"key":"8_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1007\/3-540-61604-7_84","volume-title":"CONCUR 96, Seventh Int. Conf. on Concurrency Theory, Pisa","author":"A. Maggiolo-Schettini","year":"1996","unstructured":"Andrea Maggiolo-Schettini, Andriano Peron, and Simone Tini. Equivalences of statecharts. In CONCUR 96, Seventh Int. Conf. on Concurrency Theory, Pisa, LNCS 1119, pages 687\u2013702. Springer-Verlag, 1996."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"8_CR19","series-title":"PhD thesis","volume-title":"Symbolic Model Checking. An approach to the state explosion problem","author":"K. L. McMillian","year":"1992","unstructured":"Kenneth L. McMillian. Symbolic Model Checking. An approach to the state explosion problem. PhD thesis, Carnegie Mellon University, Pittsburgh, 1992."},{"key":"8_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Theoretical Aspects of Computer Science","author":"A. Pnueli","year":"1991","unstructured":"A. Pnueli and M. Shalev. What is in a step: On the semantics of statecharts. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 526. Springer-Verlag, 1991."},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. In transition from global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series, Vol. F13, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BFb0035101","volume-title":"PARLE\u201991 Parallel Architectures and Languages","author":"G. Tel","year":"1991","unstructured":"Gerard Tel and Friedemann Mattern. The derivation of distributed termination detection algorithms from garbage collection schemes. In E.H.L. Aarts, J. van Leeuwen, and M. Rem, editors, PARLE\u201991 Parallel Architectures and Languages, Volume I: Parallel Architectures and Algorithms, Lecture Notes in Computer Science 505, pages 137\u2013149. Springer-Verlag, 1991."},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/BFb0014994","volume-title":"CONCUR 94","author":"A. C. Uselton","year":"1994","unstructured":"Andrew C. Uselton and Scott A. Smolka. A compositional semantics for statecharts using labeled transition systems. In CONCUR 94, LNCS 836, pages 2\u201317. Springer-Verlag, 1994."},{"key":"8_CR24","series-title":"Lect Notes Comput Sci","first-page":"128","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Beek van der","year":"1994","unstructured":"M. van der Beek. A comparison of statechart variants. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pages 128\u2013148. Springer-Verlag, 1994."}],"container-title":["Lecture Notes in Computer Science","Compositionality: The Significant Difference"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49213-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T16:14:25Z","timestamp":1557072865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49213-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654933","9783540492139"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-49213-5_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}