{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T23:03:33Z","timestamp":1774479813233,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319406473","type":"print"},{"value":"9783319406480","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_2","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"19-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["On Implementing Real-Time Specification Patterns Using Observers"],"prefix":"10.1007","author":[{"given":"John D.","family":"Backes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Komp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420. IEEE (1999)","DOI":"10.1145\/302405.302672"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372\u2013381. ACM (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.entcs.2005.10.035","volume":"153","author":"V Gruhn","year":"2006","unstructured":"Gruhn, V., Laue, R.: Patterns for timed property specifications. Electron. Notes Theoret. Comput. Sci. 153, 117\u2013133 (2006)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jss.2008.06.041","volume":"82","author":"P Bellini","year":"2009","unstructured":"Bellini, P., Nesi, P., Rogai, D.: Expressing and organizing real-time specification patterns via temporal logics. J. Syst. Softw. 82, 183\u2013196 (2009)","journal-title":"J. Syst. Softw."},{"key":"2_CR5","unstructured":"Reinkemeier, P., Stierand, I., Rehkop, P., Henkler, S.: A pattern-based requirement specification language: mapping automotive specific timing requirements. In: Fachtagung des GI-Fachbereichs Softwaretechnik, pp. 99\u2013108 (2011)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Etzien, C., Gezgin, T., Froschle, S., Henkler, S., Rettberg, A.: Contracts for evolving systems. In: ISORC, pp. 1\u20138 (2013)","DOI":"10.1109\/ISORC.2013.6913235"},{"key":"2_CR7","unstructured":"Alur, R.: Techniques for automatic verification of real-time systems. Ph.D. thesis, stanford university (1991)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time Syst. 2, 255\u2013299 (1990)","journal-title":"Real-time Syst."},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/237432.237438","volume":"6","author":"LE Moser","year":"1997","unstructured":"Moser, L.E., Ramakrishna, Y., Kutty, G., Melliar-Smith, P.M., Dillon, L.K.: A graphical environment for the design of concurrent real-time systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 6, 31\u201379 (1997)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32469-7_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"N Abid","year":"2012","unstructured":"Abid, N., Dal Zilio, S., Le Botlan, D.: Real-time specification patterns and tools. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 1\u201315. Springer, Heidelberg (2012)"},{"key":"2_CR11","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 dataflow programming language LUSTRE. Proc. IEEE 79, 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","volume-title":"NASA Formal Methods","author":"J Backes","year":"2015","unstructured":"Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82\u201396. Springer, Heidelberg (2015)"},{"key":"2_CR13","unstructured":"Murugesan, A., Heimdahl, M.P., Whalen, M.W., Rayadurgam, S., Komp, J., Duan, L., Kim, B.G., Sokolsky, O., Lee, I.: From requirements to code: model based development of a medical cyber physical system. SEHC (2014)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012)"},{"key":"2_CR15","volume-title":"Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language","author":"PH Feiler","year":"2012","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edn. Addison-Wesley Professional, Reading (2012)","edition":"1"},{"key":"2_CR16","unstructured":"CESAR: The CESAR project (2010). \n                      http:\/\/www.cesarproject.eu\/"},{"key":"2_CR17","unstructured":"Dutertre, B., Sorea, M.: Timed systems in SAL. Technical report, SRI International (2004)"},{"key":"2_CR18","unstructured":"Pike, L.: Real-time system verification by \n                      \n                        \n                      \n                      $$k$$\n                    -induction. Technical report, NASA (2005)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Gao, J., Whalen, M., Van Wyk, E.: Extending lustre with timeout automata. In: SLA++P (2007)","DOI":"10.1016\/j.entcs.2008.05.014"},{"key":"2_CR20","unstructured":"Gacek, A., Backes, J., Whalen, M.W., Cofer, D.: AGREE Users Guide (2014). \n                      http:\/\/github.com\/smaccm\/smaccm"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-75454-1_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R G\u00f3mez","year":"2007","unstructured":"G\u00f3mez, R., Bowman, H.: Efficient detection of zeno runs in timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 195\u2013210. Springer, Heidelberg (2007)"},{"key":"2_CR22","unstructured":"Gafni, V., Benveniste, A., Caillaud, B., Graf, S., Josko, B.: Contract specification language (CSL). Technical report, SPEEDS Deliverable D.2.5.4 (2008)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: Formal Methods in Computer-Aided Design, pp. 231\u2013238 (2007)","DOI":"10.1109\/FAMCAD.2007.10"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Sorea, M., Dutertre, B., Steiner, W.: Modeling and verification of time-triggered communication protocols. In: 2008 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 422\u2013428. IEEE (2008)","DOI":"10.1109\/ISORC.2008.52"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Li, W., Grard, L., Shankar, N.: Design and verification of multi-rate distributed systems. In: 2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 20\u201329 (2015)","DOI":"10.1109\/MEMCOD.2015.7340463"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T00:48:22Z","timestamp":1558313302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"4 June 2016","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":"Minneapolis","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":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 June 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 June 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}