{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:17:30Z","timestamp":1749010650594,"version":"3.41.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319339504"},{"type":"electronic","value":"9783319339511"}],"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-33951-1_15","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"203-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["The PERF Approach for Formal Verification"],"prefix":"10.1007","author":[{"given":"Nazim","family":"Benaissa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Bonvoisin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abderrahmane","family":"Feliachi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Ordioni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Atelier, B.: version 3.2, manuel de r\u00e9f\u00e9rence du langage B. GEC Alsthom Transport and Steria M\u00e9diterrann\u00e9e and SNCF and INRETS and RATP (1997)","DOI":"10.1016\/S1365-6937(97)90694-8"},{"key":"15_CR2","unstructured":"DO-178C, software considerations in airborne systems and equipment certification. Special Committee 205 of RTCA (2011)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-319-05032-4_17","volume-title":"Software Engineering and Formal Methods","author":"R Abo","year":"2014","unstructured":"Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221\u2013236. Springer, Heidelberg (2014)"},{"issue":"6","key":"15_CR4","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR5","unstructured":"Bonvoisin, D., Benaissa, N.: Utilisation de la m\u00e9thode de preuve formelle PERF de la RATP sur le projet PEEE. Revue G\u00e9n\u00e9rale des Chemins de Fer 250 (2015)"},{"key":"15_CR6","unstructured":"CENELEC EN-50128: Railway applications - Communication, signalling and processing systems - software for railway control and protection systems (2011)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-39724-3_11","volume-title":"Correct Hardware Design and Verification Methods","author":"H Chockler","year":"2003","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for formal verification. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 111\u2013125. Springer, Heidelberg (2003)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Claessen, K.: A coverage analysis for safety property lists. In: Formal Methods in Computer Aided Design, November 2007","DOI":"10.1109\/FMCAD.2007.4401992"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Das, S., Basu, P., Banerjee, A., Dasgupta, P., Chakrabarti, P., Mohan, C., Fix, L., Armoni, R.: Formal verification coverage: computing the coverage gap between temporal specifications. In: ICCAD, pp. 198\u2013203, November 2004","DOI":"10.1109\/ICCAD.2004.1382571"},{"issue":"9","key":"15_CR10","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. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Pessaux, F.: FoCaLiZe: Inside an F-IDE. arXiv preprint arXiv:1404.6607 (2014)","DOI":"10.4204\/EPTCS.149.7"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isabelle\/jedit \u2013 a prover IDE within the PIDE framework. CoRR abs\/1207.3441 (2012)","DOI":"10.1007\/978-3-642-31374-5_38"},{"key":"15_CR13","unstructured":"Wenzel, M.: PIDE as front-end technology for Coq. CoRR abs\/1304.6626 (2013)"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:40:22Z","timestamp":1748986822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"15 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}