{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:36:12Z","timestamp":1780115772200,"version":"3.54.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,5,18]],"date-time":"2009-05-18T00:00:00Z","timestamp":1242604800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1007\/s11334-009-0089-0","type":"journal-article","created":{"date-parts":[[2009,5,17]],"date-time":"2009-05-17T04:17:29Z","timestamp":1242533849000},"page":"139-148","source":"Crossref","is-referenced-by-count":1,"title":["A formal model of composing components: the TLA+ approach"],"prefix":"10.1007","volume":"5","author":[{"given":"Ondrej","family":"Rysavy","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jaroslav","family":"Rab","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2009,5,18]]},"reference":[{"issue":"1","key":"89_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi M, Lamport L (1993) Composing specifications. ACM Trans Program Lang Syst 15(1): 73\u2013132","journal-title":"ACM Trans Program Lang Syst"},{"key":"89_CR2","unstructured":"Abadi M, Lamport L (1993) Conjoining specifications. Research Report 118, Digital Equipment Corporation"},{"key":"89_CR3","first-page":"499","volume-title":"Mathematical foundations of computer science. Lecture notes in computer science, vol 969","author":"M Abadi","year":"1995","unstructured":"Abadi M, Merz S (1995) An abstract account of composition. In: Wiedermann J, Hajek P (eds) Mathematical foundations of computer science. Lecture notes in computer science, vol 969. Springer, Prague, pp 499\u2013508"},{"key":"89_CR4","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-45449-7_8","volume-title":"Verification of embedded software: problems and perspectives. Lecture notes in computer science, vol 2211","author":"P Cousot","year":"2001","unstructured":"Cousot P, Cousot R (2001) Verification of embedded software: problems and perspectives. Lecture notes in computer science, vol 2211. Springer, Berlin, pp 97\u2013114"},{"key":"89_CR5","doi-asserted-by":"crossref","unstructured":"Diaconescu R, Futatsugi K, Iida S (1999) Component-based algebraic specification and verification in cafeobj. In: FM\u201999\u2014formal methods. Lecture notes in computer science, vol 1709. Springer, Berlin, pp 1644\u20131663","DOI":"10.1007\/3-540-48118-4_37"},{"key":"89_CR6","unstructured":"Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni-Vincentelli AL (2006) Hierarchical timing language. Technical Report Technical Report No. UCB\/EECS-20, EECS Department, University of California, Berkeley"},{"key":"89_CR7","doi-asserted-by":"crossref","unstructured":"Henzinger TA (2000) Masaccio: a formal model for embedded components. In: TCS \u201900: Proceedings of the international conference IFIP on theoretical computer science, exploring new frontiers of theoretical informatics. Springer, London, pp 549\u2013563","DOI":"10.1007\/3-540-44929-9_38"},{"key":"89_CR8","first-page":"166","volume-title":"Giotto: a time-triggered language for embedded programming. Lecture notes in computer science, vol 2211","author":"TA Henzinger","year":"2001","unstructured":"Henzinger TA, Horowitz B, Kirsch CM (2001) Giotto: a time-triggered language for embedded programming. Lecture notes in computer science, vol 2211. Springer, Berlin, pp 166\u2013184"},{"key":"89_CR9","first-page":"275","volume-title":"Hybrid systems: computation and control. Lecture notes in computer science, chapter Assume-guarantee reasoning for hierarchical hybrid systems, vol 2034","author":"TA Henzinger","year":"2001","unstructured":"Henzinger TA, Minea M, Prabbu V (2001) Hybrid systems: computation and control. Lecture notes in computer science, chapter Assume-guarantee reasoning for hierarchical hybrid systems, vol 2034. Springer, Berlin, pp 275\u2013290"},{"key":"89_CR10","doi-asserted-by":"crossref","unstructured":"Herrmann P, Graw G, Krumm H (1998) Compositional specification and structured verification of hybrid systems in ctla. In: Proceedings of 1st IEEE international symposium on object-oriented real-time distributed computing. IEEE Computer Society Press, New York, pp 335\u2013340","DOI":"10.1109\/ISORC.1998.666805"},{"key":"89_CR11","doi-asserted-by":"crossref","unstructured":"Hooman J (1993) A compositional approach to the design of hybrid systems. In: Hybrid systems. Springer, London, pp 121\u2013148","DOI":"10.1007\/3-540-57318-6_27"},{"issue":"6","key":"89_CR12","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1093\/logcom\/13.6.921","volume":"13","author":"M Kaminski","year":"2001","unstructured":"Kaminski M, Yariv Y (2001) A real-time semantics of temporal logic of actions. J Logic Comput 13(6): 921\u2013937","journal-title":"J Logic Comput"},{"key":"89_CR13","first-page":"285","volume-title":"Real-time systems: design principles for distributed embedded applications. The Springer international series in engineering and computer science, chapter The time-triggered architecture, vol 395","author":"H Kopetz","year":"2002","unstructured":"Kopetz H (2002) Real-time systems: design principles for distributed embedded applications. The Springer international series in engineering and computer science, chapter The time-triggered architecture, vol 395. Springer, Netherlands, pp 285\u2013297"},{"issue":"3","key":"89_CR14","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/0890-5401(88)90020-X","volume":"79","author":"R Koymans","year":"1988","unstructured":"Koymans R, Shyamasundar RK, de Roever WP, Gerth R, Arun-Kumar S (1988) Compositional semantics for real-time distributed computing. Inf Comput 79(3): 210\u2013256","journal-title":"Inf Comput"},{"key":"89_CR15","unstructured":"Lamport L (1992) Hybrid systems in tla+. In: Hybrid systems. Lecture notes in computer science, vol 736. Springer, Berlin, pp 77\u2013102"},{"key":"89_CR16","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2003","unstructured":"Lamport L (2003) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading"},{"issue":"1","key":"89_CR17","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.entcs.2006.07.003","volume":"163","author":"K-K Lau","year":"2006","unstructured":"Lau K-K, Ukis V, Velasco P, Wang Z (2006) A component model for separation of control flow from computation in component-based systems. Electron Notes Theor Comput Sci 163(1): 57\u201369","journal-title":"Electron Notes Theor Comput Sci"},{"key":"89_CR18","volume-title":"Advances in computers, chapter Embedded software","author":"E Lee","year":"2002","unstructured":"Lee E (2002) Advances in computers, chapter Embedded software. Academic Press, New York"},{"key":"89_CR19","first-page":"196","volume-title":"Hybrid i\/o automata. Lecture notes in computer science","author":"N Lynch","year":"1996","unstructured":"Lynch N, Segala R, Vaandrager F (1996) Hybrid i\/o automata. Lecture notes in computer science. Springer, Berlin, pp 196\u2013510"},{"key":"89_CR20","unstructured":"Ramakrishna YS, Shyamasundar RK (1995) A compositional semantics of esterel in duration calculus. In: Proceedings of second AMAST workshop on real-time systems: models and proofs, bordeux. Springer, Berlin"},{"key":"89_CR21","doi-asserted-by":"crossref","unstructured":"Rysavy O, Rab J (2008) A component-based approach to verification of embedded control systems using tla. In: IEEE proceedings of international multiconference on computer science and information technology. IEEE Computer Society Press, New York, pp 719\u2013725","DOI":"10.1109\/IMCSIT.2008.4747321"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0089-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-009-0089-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0089-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:44Z","timestamp":1559396864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0089-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,5,18]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["89"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0089-0","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,5,18]]}}}