{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:35:13Z","timestamp":1742938513500,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319054155"},{"type":"electronic","value":"9783319054162"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05416-2_17","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"262-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Precise Documentation and Validation of Requirements"],"prefix":"10.1007","author":[{"given":"Chen-Wei","family":"Wang","sequence":"first","affiliation":[]},{"given":"Jonathan S.","family":"Ostroff","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Hudon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"17_CR2","series-title":"LNCS","first-page":"242","volume-title":"B 2002 and ZB 2002","author":"J-R Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 242\u2013269. Springer, Heidelberg (2002)"},{"key":"17_CR3","series-title":"LNCS","first-page":"337","volume-title":"TACAS 2008","author":"LM de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"17_CR4","series-title":"LNCS","first-page":"494","volume-title":"NFM 2011","author":"C Eles","year":"2011","unstructured":"Eles, C., Lawford, M.: A tabular expression toolbox for matlab\/simulink. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 494\u2013499. Springer, Heidelberg (2011)"},{"issue":"3","key":"17_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/52.896248","volume":"17","author":"CA Gunter","year":"2000","unstructured":"Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Softw. 17(3), 37\u201343 (2000)","journal-title":"IEEE Softw."},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012)","journal-title":"ACM Comput. Surv."},{"key":"17_CR7","unstructured":"IEEE: IEEE standard for transitions, pulses, and related waveforms. IEEE Std 181-2011 (Revision of IEEE Std 181-2003), pp. 1\u201371 (2011)"},{"key":"17_CR8","unstructured":"Jackson, M.: Software Requirements Specifications: A Lexicon of Practice, Principles and Prejudices. Addison-Wesley, New York (1995)"},{"key":"17_CR9","volume-title":"Reflections on the Work of C. A. R. Hoare","author":"M Jackson","year":"2010","unstructured":"Jackson, M.: The operational principle and problem frames. Reflections on the Work of C. A. R. Hoare. Springer, London (2010)"},{"issue":"11","key":"17_CR10","doi-asserted-by":"publisher","first-page":"980","DOI":"10.1016\/j.scico.2009.12.009","volume":"75","author":"Y Jin","year":"2010","unstructured":"Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program. 75(11), 980\u20131000 (2010)","journal-title":"Sci. Comput. Program."},{"key":"17_CR11","unstructured":"Lawford, M., Froebel, P., Moum, G.: Application of tabular methods to the specification and verification of a nuclear reactor shutdown system. Formal Meth. Syst. Des. (2000). http:\/\/www.cas.mcmaster.ca\/~lawford\/papers\/FMSD.html"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.4204\/EPTCS.43.4","volume":"43","author":"I Maamria","year":"2010","unstructured":"Maamria, I., Butler, M.: Rewriting and well-definedness within a proof system. EPTCS 43, 49\u201364 (2010)","journal-title":"EPTCS"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1109\/MC.2008.37","volume":"41","author":"TSE Maibaum","year":"2008","unstructured":"Maibaum, T.S.E., Wassyng, A.: A product-focused approach to software certification. IEEE Comput. 41(2), 91\u201393 (2008)","journal-title":"IEEE Comput."},{"key":"17_CR14","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New Jersey (1997)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Misra, J.: A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer, New York (2001)","DOI":"10.1007\/978-1-4419-8528-6_11"},{"issue":"3","key":"17_CR16","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1049\/ip-sen:20000681","volume":"147","author":"JS Ostroff","year":"2000","unstructured":"Ostroff, J.S., Paige, R.F.: The logic of software design. Proc. IEE - Softw. 147(3), 72\u201380 (2000)","journal-title":"Proc. IEE - Softw."},{"key":"17_CR17","unstructured":"Ostroff, J.S., Wang, C.-W., Hudon, S.: Precise documentation of requirements and executable specifications. Technical Report CSE-2012-03, York University (2012)"},{"key":"17_CR18","unstructured":"Ostroff, J.S., Wang, C.-W., Hudon, S.: Precise documentation and validation of requirements. Technical Report CSE-2013-08, York University (2013)"},{"issue":"9","key":"17_CR19","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1109\/32.241769","volume":"19","author":"DL Parnas","year":"1993","unstructured":"Parnas, D.L.: Predicate logic for software engineering. IEEE Trans. Softw. Eng. 19(9), 856\u2013862 (1993)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0167-6423(95)96871-J","volume":"25","author":"DL Parnas","year":"1995","unstructured":"Parnas, D.L., Madey, J.: Functional documentation for computer systems. Sci. Comput. Prog. 25, 41\u201361 (1995)","journal-title":"Sci. Comput. Prog."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: FME, pp. 133\u2013153 (2003)","DOI":"10.1007\/978-3-540-45236-2_9"},{"issue":"4\u20135","key":"17_CR22","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10009-005-0209-6","volume":"8","author":"A Wassyng","year":"2006","unstructured":"Wassyng, A., Lawford, M.: Software tools for safety-critical software development. STTT 8(4\u20135), 337\u2013354 (2006)","journal-title":"STTT"},{"key":"17_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11526841_12","volume-title":"FM 2005","author":"A Wassyng","year":"2005","unstructured":"Wassyng, A., Lawford, M., Hu, X.: Timing tolerances in safety-critical software. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 157\u2013172. Springer, Heidelberg (2005)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05416-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T08:13:34Z","timestamp":1720772014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_17","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 April 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}