{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T07:06:22Z","timestamp":1770447982320,"version":"3.49.0"},"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_28","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"373-387","source":"Crossref","is-referenced-by-count":8,"title":["From Design Contracts to Component Requirements Verification"],"prefix":"10.1007","author":[{"given":"Jing","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John D.","family":"Backes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Darren","family":"Cofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"28_CR2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MS.2012.173","volume":"30","author":"MW Whalen","year":"2013","unstructured":"Whalen, M.W., Gacek, A., Cofer, D.D., Murugesan, A., Heimdahl, M.P.E., Rayadurgam, S.: Your \u201cwhat\u201d is my \u201chow\u201d: Iteration and hierarchy in system design. IEEE Softw. 30, 54\u201360 (2013)","journal-title":"IEEE Softw."},{"key":"28_CR3","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, Boston (2012)","edition":"1"},{"key":"28_CR4","unstructured":"MathWorks: Simulink (2016). http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"28_CR5","unstructured":"RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Washington, DC (2011)"},{"key":"28_CR6","unstructured":"RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A, Washington, DC (2011)"},{"key":"28_CR7","unstructured":"RTCA DO-331: Model-Based Development and Verification Supplement to DO-178C and DO-278A, Washington, DC (2011)"},{"key":"28_CR8","unstructured":"Cofer, D., Miller, S.P.: Formal methods case studies for DO-333, NASA contractor report NASA\/CR-2014-218244 (2014)"},{"key":"28_CR9","unstructured":"MathWorks: Simulink (2016). http:\/\/www.mathworks.com\/products\/sldesignverifier\/"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: ACM International Conference on High Integrity Language Technology (HILT) 2013. ACM (2013)","DOI":"10.1145\/2527269.2527272"},{"key":"28_CR11","doi-asserted-by":"crossref","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":"28_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)","edition":"2"},{"key":"28_CR13","unstructured":"Backes, J., et al.: AGREE toolset (2016). http:\/\/loonwerks.com\/tools\/agree.html"},{"key":"28_CR14","unstructured":"RTCA DO-330: Software Tool Qualification Considerations, Washington, DC (2011)"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Miller, S.P., Bhattacharyya, S., Tinelli, C., Smolka, S., Sticksel, C., Meng, B., Yang, J.: Formal verification of quasi-synchronous systems. Final Technical report delivered Air Force Research Laboratory (2015)","DOI":"10.1109\/DASC.2014.6979532"},{"key":"28_CR16","unstructured":"Accident, C.A., Incident Investigation Commission\u00a0(CIAIAC), S.: Technical report: Accident occurred on 21 May 1998 to Aircraft Airbus A-320-21 Registration G-UKLL At Ibiza Airport, Balearic Islands (1998)"},{"key":"28_CR17","unstructured":"CriSys Group: Generic patient controlled analgesia infusion pump project (2016). http:\/\/crisys.cs.umn.edu\/gpca.shtml"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Wang, C., Pastore, F., Goknil, A., Briand, L., Iqbal, Z.: Automatic generation of system test cases from use case specifications. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 385\u2013396. ACM, New York (2015)","DOI":"10.1145\/2771783.2771812"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Ibrahim, R., Saringat, M., Ibrahim, N., Ismail, N.: An automatic tool for generating test cases from the system\u2019s requirements. In: 7th IEEE International Conference on Computer and Information Technology, CIT 2007, pp. 861\u2013866 (2007)","DOI":"10.1109\/CIT.2007.116"},{"key":"28_CR20","doi-asserted-by":"crossref","first-page":"1379","DOI":"10.1016\/j.jss.2011.03.051","volume":"84","author":"MJ Escalona","year":"2011","unstructured":"Escalona, M.J., Gutierrez, J.J., Mej\u00edas, M., Arag\u00f3n, G., Ramos, I., Torres, J., Dom\u00ednguez, F.J.: An overview on test generation from functional requirements. J. Syst. Softw. 84, 1379\u20131393 (2011)","journal-title":"J. Syst. Softw."},{"key":"28_CR21","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf. 8, 303\u2013319 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"28_CR22","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.ress.2014.07.003","volume":"132","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., Cimatti, A., Katoen, J., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20\u201335 (2014)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Silva, W., Bezerra, E., Winterholer, M., Lettnin, D.: Automatic property generation for formal verification applied to hdl-based design of an on-board computer for space applications. In: 2013 14th Latin American Test Workshop (LATW), pp. 1\u20136 (2013)","DOI":"10.1109\/LATW.2013.6562663"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Soeken, M., Kuhne, U., Freibothe, M., Fe, G., Drechsler, R.: Automatic property generation for the formal verification of bus bridges. In: 2011 IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits Systems (DDECS), pp. 417\u2013422 (2011)","DOI":"10.1109\/DDECS.2011.5783129"},{"key":"28_CR25","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. Part 3 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program. Part 3"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T03:11:37Z","timestamp":1567998697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}