{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T18:28:32Z","timestamp":1766428112523,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031067723"},{"type":"electronic","value":"9783031067730"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_19","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"355-372","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Assume-Guarantee Reasoning with\u00a0Scheduled Components"],"prefix":"10.1007","author":[{"given":"Cong","family":"Liu","sequence":"first","affiliation":[]},{"given":"Junaid","family":"Babar","sequence":"additional","affiliation":[]},{"given":"Isaac","family":"Amundson","sequence":"additional","affiliation":[]},{"given":"Karl","family":"Hoech","sequence":"additional","affiliation":[]},{"given":"Darren","family":"Cofer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2264-2958","authenticated-orcid":false,"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-40648-0_2","volume-title":"NASA Formal Methods","author":"JD Backes","year":"2016","unstructured":"Backes, J.D., Whalen, M.W., Gacek, A., Komp, J.: On implementing real-time specification patterns using observers. In: International Symposium on NASA Formal Methods. pp. 19\u201333. Springer (2016)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Baker, T., Shaw, A.: The cyclic executive model and Ada. In: Real-Time Systems Symposium, pp. 120\u2013129. IEEE (1988)","DOI":"10.1109\/REAL.1988.51108"},{"issue":"2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A Benveniste","year":"1991","unstructured":"Benveniste, A., Le Guernic, P., Jacquemot, C.: Synchronous programming with events and relations: the SIGNAL language and its semantics. Science of Computer Programming 16(2), 103\u2013149 (1991)","journal-title":"Sci. Comput. Program."},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-41591-8_24","volume-title":"Software Engineering and Formal Methods","author":"A Champion","year":"2016","unstructured":"Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: A mode-aware contract language for reactive systems. In: International Conference on Software Engineering and Formal Methods. pp. 347\u2013366. Springer (2016)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification: LASER 2011, pp. 1\u201330. Springer (2012)."},{"key":"19_CR6","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Fourth Annual Symposium on Logic in Computer Science, pp. 353\u2013362. IEEE (1989)"},{"key":"19_CR7","first-page":"2","volume":"01","author":"D Cofer","year":"2022","unstructured":"Cofer, D., Amundson, I., Babar, J., Hardin, D., Slind, K., Alexander, P., Hatcliff, J., Robby, R., Klein, G., Lewis, C., Mercer, E., Shackleton, J.: Cyberassured systems engineering at scale. IEEE Secur. Priv. 01, 2\u201314 (2022)","journal-title":"IEEE Secur. Priv."},{"issue":"11","key":"19_CR8","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/MC.2018.2876051","volume":"51","author":"D Cofer","year":"2018","unstructured":"Cofer, D., Gacek, A., Backes, J., Whalen, M.W., Pike, L., Foltzer, A., Podhradsky, M., Klein, G., Kuz, I., Andronick, J., Heiser, G., Stuart, D.: A formal approach to constructing secure air vehicle software. Computer 51(11), 14\u201323 (2018)","journal-title":"Computer"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.L., Pagano, B., Pouzet, M.: SCADE 6: a formal language for embedded critical software development. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 1\u201311. IEEE (2017)","DOI":"10.1109\/TASE.2017.8285623"},{"key":"19_CR10","unstructured":"Feiler, P., Gluch, D.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. Addison-Wesley Professional (2012)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Frana, R., Bodeveix, J.P., Filali, M., Rolland, J.F.: The AADL behaviour annex - experiments and roadmap. In: International Conference on Engineering of Complex Computer Systems, pp. 377\u2013382. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L.G., Ghassabani, E.: The JKind model checker. In: International Conference on Computer Aided Verification. pp. 20\u201327. Springer (2018)"},{"issue":"9","key":"19_CR13","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proceedings of the IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual execution of AADL models via a translation into synchronous programs. In: International Conference on Embedded Software, pp. 134\u2013143. ACM (2007)","DOI":"10.1145\/1289927.1289951"},{"key":"19_CR15","unstructured":"Kahn, G.: The semantics of a simple language for parallel programming. In: Rosenfeld, J.L. (ed.) Information Processing, Proceedings of the 6th IFIP Congress 1974, pp. 471\u2013475. North-Holland (1974)"},{"key":"19_CR16","unstructured":"Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, UCLA (1968)"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"1","key":"19_CR18","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/TC.1987.5009446","volume":"36","author":"EA Lee","year":"1987","unstructured":"Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput. 36(1), 24\u201335 (1987)","journal-title":"IEEE Trans. Comput."},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Mercer, E., Slind, K., Amundson, I., Cofer, D., Babar, J., Hardin, D.: Synthesizing verified components for cyber assured systems engineering. In: 24th International Conference on Model Driven Engineering Languages and Systems, pp. 205\u2013215. IEEE (2021)","DOI":"10.1109\/MODELS50736.2021.00029"},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2012.05.040","volume":"451","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"19_CR21","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/s10009-020-00575-y","volume":"22","author":"P Metzler","year":"2020","unstructured":"Metzler, P., Suri, N., Weissenbacher, G.: Extracting safe thread schedules from incomplete model checking results. International Journal on Software Tools for Technology Transfer 22(5), 565\u2013581 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-13464-7_5","volume-title":"Formal Techniques for Distributed Systems","author":"PC \u00d6lveczky","year":"2010","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in real-time Maude. In: Hatcliff, J., Zucca, E. (eds.) Formal Techniques for Distributed Systems. pp. 47\u201362. Springer (2010)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, sub-series F: Computer and System Science, pp. 123\u2013144. Springer-Verlag (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Rasmussen, S., Kingston, D., Humphrey, L.: A brief introduction to unmanned systems autonomy services (UxAS). In: International Conference on Unmanned Aircraft Systems, pp. 257\u2013268. IEEE (2018)","DOI":"10.1109\/ICUAS.2018.8453287"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Singhoff, F., Legrand, J., Nana, L., Marc\u00e9, L.: Scheduling and memory requirements analysis with AADL. In: Annual ACM SIGAda International Conference on Ada, pp. 1\u201310. ACM (2005)","DOI":"10.1145\/1104011.1103847"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., Gacek, A., Cofer, D., Murugesan, A., Heimdahl, M.P., Rayadurgam, S.: Your what is my how: iteration and hierarchy in system design. IEEE Softw. 30(2), 54\u201360 (2013)","DOI":"10.1109\/MS.2012.173"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,25]],"date-time":"2024-09-25T14:24:39Z","timestamp":1727274279000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"118","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}