{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:10:02Z","timestamp":1746177002564,"version":"3.40.4"},"publisher-location":"Cham","reference-count":25,"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_9","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"125-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formalizing and Verifying Function Blocks Using Tabular Expressions and PVS"],"prefix":"10.1007","author":[{"given":"Linna","family":"Pang","sequence":"first","affiliation":[]},{"given":"Chen-Wei","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Lawford","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Wassyng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"key":"9_CR1","unstructured":"Bakhmach, E., Siora, O., Tokarev, V., Reshetytskyi, S., Kharchenko, V., Bezsalyi, V.: FPGA - based technology and systems for I&C of existing and advanced reactors. International Atomic Energy Agency, p. 173 (2009), IAEA-CN-164-7S04"},{"key":"9_CR2","series-title":"LNCS","first-page":"517","volume-title":"INT 2004","author":"N Bauer","year":"2004","unstructured":"Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 517\u2013540. Springer, Heidelberg (2004)"},{"key":"9_CR3","unstructured":"Blech, J.O., Biha, S.O.: On formal reasoning on the semantics of PLC using Coq. CoRR abs\/1301.3047 (2013)"},{"key":"9_CR4","unstructured":"Camilleri, A., Gordon, M., Melham, T.: Hardware verification using higher-order logic. Technical Report UCAM-CL-TR-91, Cambridge University Computer Lab (1986)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: IEEE International Conference on Systems, Man and Cybernetics, pp. 2449\u20132454 (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Eles, C., Lawford, M.: A tabular expression toolbox for Matlab\/Simulink. In: NASA Formal Methods, pp. 494\u2013499 (2011)","DOI":"10.1007\/978-3-642-20398-5_38"},{"key":"9_CR7","series-title":"LNCS","first-page":"119","volume-title":"FMICS 2008","author":"X Hu","year":"2009","unstructured":"Hu, X., Lawford, M., Wassyng, A.: Formal verification of the implementability of timing requirements. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 119\u2013134. Springer, Heidelberg (2009)"},{"key":"9_CR8","unstructured":"IEC: 61131\u20133 Ed. 2.0 en:2003: Programmable Controllers \u2013 Part 3: Programming Languages. International Electrotechnical Commission (2003)"},{"key":"9_CR9","unstructured":"IEC: 61131\u20133 Ed. 3.0 en:2013: Programmable Controllers \u2013 Part 3: Programming Languages. International Electrotechnical Commission (2013)"},{"issue":"11","key":"9_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":"9_CR11","volume-title":"IEC 61131\u20133: Programming Industrial Automation Systems Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids","author":"KH John","year":"2010","unstructured":"John, K.H., Tiegelkamp, M.: IEC 61131\u20133: Programming Industrial Automation Systems Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids, 2nd edn. Springer, Heidelberg (2010)","edition":"2"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Kabra, A., Bhattacharjee, A., Karmakar, G., Wakankar, A.: Formalization of sequential function chart as synchronous model in Lustre. In: NCETACS, pp. 115\u2013120 (2012)","DOI":"10.1109\/NCETACS.2012.6203309"},{"key":"9_CR13","series-title":"LNCS","first-page":"73","volume-title":"AMAST 2000","author":"M Lawford","year":"2000","unstructured":"Lawford, M., McDougall, J., Froebel, P., Moum, G.: Practical application of functional and relational methods for the specification and verification of safety critical software. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, p. 73. Springer, Heidelberg (2000)"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s11704-010-0026-2","volume":"4","author":"Z Liu","year":"2010","unstructured":"Liu, Z., Parnas, D., Widemann, B.: Documenting and verifying systems assembled from components. Front. Comput. Sci. China 4(2), 151\u2013161 (2010)","journal-title":"Front. Comput. Sci. China"},{"key":"9_CR15","unstructured":"Mader, A., Wupper, H.: Timed automaton models for simple programmable logic controllers. In: ECRTS, pp. 114\u2013122. IEEE (1999)"},{"key":"9_CR16","first-page":"129","volume-title":"VLSI Specification, Verification and Synthesis","author":"T Melham","year":"1987","unstructured":"Melham, T.: Abstraction mechanisms for hardware verification. VLSI Specification, Verification and Synthesis, pp. 129\u2013157. Kluwer Academic Publishers, Boston (1987)"},{"key":"9_CR17","series-title":"LNCS","first-page":"199","volume-title":"FMICS 2008","author":"E N\u00e9meth","year":"2009","unstructured":"N\u00e9meth, E., Bartha, T.: Formal verification of safety functions by reinterpretation of functional block based specifications. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 199\u2013214. Springer, Heidelberg (2009)"},{"key":"9_CR18","series-title":"LNCS","first-page":"748","volume-title":"CADE 1992","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Pang, L., Wang, C.W., Lawford, M., Wassyng, A.: Formalizing and verifying function blocks using tabular expressions and PVS. Technical Report 11, McSCert, Aug 2013","DOI":"10.1007\/978-3-319-05416-2_9"},{"issue":"1","key":"9_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 documents for computer systems. Sci. Comput. Program. 25(1), 41\u201361 (1995)","journal-title":"Sci. Comput. Program."},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"948","DOI":"10.1109\/32.368133","volume":"20","author":"DL Parnas","year":"1994","unstructured":"Parnas, D.L., Madey, J., Iglewski, M.: Precise documentation of well-structured programs. IEEE Trans. Softw. Eng. 20, 948\u2013976 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Roussel, J.M., Faure, J.: An algebraic approach for PLC programs verification. In: 6th International Workshop on Discrete Event Systems, pp. 303\u2013308 (2002)","DOI":"10.1109\/WODES.2002.1167703"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/j.arcontrol.2012.09.015","volume":"36","author":"D Soliman","year":"2012","unstructured":"Soliman, D., Thramboulidis, K., Frey, G.: Transformation of function block diagrams to Uppaal timed automata for the verification of safety applications. Ann. Rev. Control 36, 338\u2013345 (2012)","journal-title":"Ann. Rev. Control"},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0167-6423(01)00028-4","volume":"42","author":"N V\u00f6lker","year":"2002","unstructured":"V\u00f6lker, N., Kr\u00e4mer, B.J.: Automated verification of function block-based industrial control systems. Sci. Comput. Program. 42(1), 101\u2013113 (2002)","journal-title":"Sci. Comput. Program."},{"key":"9_CR25","unstructured":"Wassyng, A., Janicki, R.: Tabular expressions in software engineering. In: Proceedings of ICSSEA\u201903, Paris, France, vol. 4, pp. 1\u201346 (2003)"}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:47:00Z","timestamp":1746175620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_9","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"}}]}}