{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:41Z","timestamp":1725573881631},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_12","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:35:57Z","timestamp":1294396557000},"page":"187-205","source":"Crossref","is-referenced-by-count":0,"title":["Formalising an Integrated Language in PVS"],"prefix":"10.1007","author":[{"given":"Gwen","family":"Sala\u00fcn","sequence":"first","affiliation":[]},{"given":"Christian","family":"Attiogb\u00e9","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"12_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E. Astesiano","year":"2002","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science\u00a0286(2), 153\u2013196 (2002)","journal-title":"Theoretical Computer Science"},{"key":"12_CR2","unstructured":"Attiogb\u00e9, C., Francheteau, A., Limousin, J., Sala\u00fcn, G.: ISA, a Tool for Integrated Specifications Animation, Available at \n                    \n                      http:\/\/www.sciences.univ-nantes.fr\/info\/perso\/permanents\/salaun\/ISA\/isa.html"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/3-540-49059-0_19","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"T. Basten","year":"1999","unstructured":"Basten, T., Hooman, J.: Process Algebra in PVS. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 270\u2013284. Springer, Heidelberg (1999)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-45648-1_18","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-P. Bodeveix","year":"2002","unstructured":"Bodeveix, J.-P., Filali, M.: Type Synthesis in B and the Translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 350\u2013369. Springer, Heidelberg (2002)"},{"key":"12_CR5","first-page":"32","volume-title":"Proc. of the B Users Group Meeting \u2013 Applying B in an industrial context: Tools, Lessons nd Techniques (FM 1999)","author":"J.-P. Bodeveix","year":"1999","unstructured":"Bodeveix, J.-P., Filali, M., Mu\u00f1oz, C.: A Formalization of the B Method in Coq and PVS. In: Proc. of the B Users Group Meeting \u2013 Applying B in an industrial context: Tools, Lessons nd Techniques (FM 1999), pp. 32\u201348. Springer, Heidelberg (1999)"},{"key":"12_CR6","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. In: van Eijk, P.H.J., Vissers, C.A., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 23\u201373. Elsevier Science Publishers North-Holland (1989)"},{"key":"12_CR7","series-title":"IFIP TC10\/WG 10.2","first-page":"129","volume-title":"Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M.J.C., Herbert, J., van Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, The Netherlands. IFIP TC10\/WG 10.2, pp. 129\u2013156. North-Holland, Amsterdam (1992)"},{"key":"12_CR8","unstructured":"Brooke, P.: A Timed Semantics for a Hierarchical Design Notation. PhD Thesis, University of York (1999)"},{"issue":"1","key":"12_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/comjnl\/45.1.55","volume":"45","author":"M. Calder","year":"2002","unstructured":"Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS Based on Symbolic Transition Systems. The Computer Journal\u00a045(1), 55\u201361 (2002)","journal-title":"The Computer Journal"},{"key":"12_CR10","series-title":"IFIP Conference Proceedings","first-page":"184","volume-title":"Proc. of the International Conference on Formal Description Techniques for Networked and Distributed Systems (FORTE 2001)","author":"M. Calder","year":"2001","unstructured":"Calder, M., Shankland, C.: A Symbolic Semantics and Bisimulation for Full LOTOS. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proc. of the International Conference on Formal Description Techniques for Networked and Distributed Systems (FORTE 2001), Korea. IFIP Conference Proceedings, vol.\u00a0197, pp. 184\u2013200. Kluwer Academic Publishers, Dordrecht (2001)"},{"key":"12_CR11","unstructured":"Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century (Version 1.2). Department of Computer Science, North Carolina State University (2000)"},{"key":"12_CR12","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A Tutorial Introduction to PVS. In: Proc. of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT 1995), USA. Computer Science Laboratory, SRI International (1995)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Using a PVS Embedding of CSP to Verify Authentication Protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 121\u2013136. Springer, Heidelberg (1997)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J.-C. Fernandez","year":"1996","unstructured":"Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 437\u2013440. Springer, Heidelberg (1996)"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Proc. of the 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997)","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: a Combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Proc. of the 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), UK, pp. 423\u2013438. Chapman and Hall, Boca Raton (1997)"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1109\/ICFEM.1997.630434","volume-title":"Proc. of the 1st International Conference onf Formal Engineering Methods (ICFEM 1997)","author":"J. Galloway","year":"1997","unstructured":"Galloway, J., Stoddart, W.: An Operational Semantics for ZCCS. In: Hinchey, M.G., Liu, S. (eds.) Proc. of the 1st International Conference onf Formal Engineering Methods (ICFEM 1997), Japan, pp. 272\u2013282. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"12_CR17","unstructured":"Garland, S.J., Guttag, J.V.: A Guide to LP, the Larch Prover. Technical Report, Palo Alto, California (1991)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/3-540-56883-2_15","volume-title":"Functional Programming, Concurrency, Simulation and Automated Reasoning","author":"S.J. Garland","year":"1993","unstructured":"Garland, S.J., Guttag, J.V., Horning, J.J.: An Overview of Larch. In: Lauer, P.E. (ed.) Functional Programming, Concurrency, Simulation and Automated Reasoning. LNCS, vol.\u00a0693, pp. 329\u2013348. Springer, Heidelberg (1993)"},{"key":"12_CR19","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"12_CR20","unstructured":"Gravell, A.M., Pratten, C.H.: Embedding a Formal Notation: Experiences of Automating the Embedding of Z in the Higher Order Logics of PVS and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 73\u201384. Springer, Heidelberg (1998)"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1016\/B978-044482830-9\/50025-4","volume-title":"Handbook of Process Algebra","author":"A. Ing\u00f3lfsd\u00f3ttir","year":"2001","unstructured":"Ing\u00f3lfsd\u00f3ttir, A., Lin, H.: A Symbolic Approach to Value-Passing Processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 427\u2013478. Elsevier, Amsterdam (2001)"},{"key":"12_CR22","unstructured":"ISO. LOTOS: a Formal Description Technique based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, International Standards Organisation (1989)"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic Laws for Non-Determinism and Concurrency. Journal of the ACM\u00a032, 137\u2013161 (1985)","journal-title":"Journal of the ACM"},{"key":"12_CR24","unstructured":"Maharaj, S.: A PVS Theory of Symbolic Transition Systems. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 255\u2013266. Springer, Heidelberg (2001)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Mahony, B., Dong, J.S.: Blending Object-Z and Timed CSP: An Introduction to TCOZ. In: Proc. of the International Conference on Software Engineering (ICSE 1998), Japan, pp. 95\u2013104. IEEE Computer Society Press \/ ACM Press (1998)","DOI":"10.1109\/ICSE.1998.671106"},{"issue":"1","key":"12_CR26","first-page":"50","volume":"1","author":"T.F. Melham","year":"1995","unstructured":"Melham, T.F.: A Mechanized Theory of the \u03c0-calculus in HOL. Nordic Journal of Computing\u00a01(1), 50\u201376 (1995)","journal-title":"Nordic Journal of Computing"},{"key":"12_CR27","series-title":"International Series in Computer Science","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/3-540-48119-2_26","volume-title":"FM\u201999 - Formal Methods","author":"C. Mu\u00f1oz","year":"1999","unstructured":"Mu\u00f1oz, C., Rushby, J.: Structural Embeddings: Mechanization with Method. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 452\u2013471. Springer, Heidelberg (1999)"},{"issue":"2","key":"12_CR29","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s001650050046","volume":"11","author":"M. Nesi","year":"1999","unstructured":"Nesi, M.: Formalising a Value-Passing Calculus in HOL. Formal Aspects of Computing\u00a011(2), 160\u2013199 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1007\/3-540-55602-8_201","volume-title":"Automated Deduction - CADE-11","author":"T. Nipkow","year":"1992","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 673\u2013676. Springer, Heidelberg (1992)"},{"key":"12_CR31","unstructured":"Pratten, C.H.: An Introduction to Proving AMN Specifications with PVS and the AMNPROOF Tool. In: Habrias, H. (ed.) Proc. of Z Twenty Years on - What is its Future, France, pp. 149\u2013165 (1995)"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1109\/APSEC.2001.991491","volume-title":"Proc. of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001)","author":"G. Sala\u00fcn","year":"2001","unstructured":"Sala\u00fcn, G., Allemand, M., Attiogb\u00e9, C.: Formal Framework for a Generic Combination of a Process Algebra with an Algebraic Specification Language: an Overview. In: Proc. of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), Macau, pp. 299\u2013302. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"12_CR33","first-page":"385","volume-title":"Proc. of the 26th Annual International Computer Software and Applications Conference (COMPSAC 2002)","author":"G. Sala\u00fcn","year":"2002","unstructured":"Sala\u00fcn, G., Allemand, M., Attiogb\u00e9, C.: A Method to Combine any Process Algebra with an Algebraic Specification Language: the \u03c0-Calculus Example. In: Proc. of the 26th Annual International Computer Software and Applications Conference (COMPSAC 2002), England, pp. 385\u2013390. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"12_CR34","volume-title":"Proc. of the 7th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA 2002)","author":"G. Sala\u00fcn","year":"2002","unstructured":"Sala\u00fcn, G., Allemand, M., Attiogb\u00e9, C.: Specification of an Access Control System with a Formalism Combining CCS and CASL. In: Proc. of the 7th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA 2002). IEEE Computer Society Press, USA (2002)"},{"key":"12_CR35","unstructured":"Sala\u00fcn, G., Attiogb\u00e9, C., Allemand, M.: Verification of Integrated Specifications using PVS. Technical Report 03.02, University of Nantes (February 2003), Available at \n                    \n                      http:\/\/www.sciences.univ-nantes.fr\/info\/perso\/permanents\/salaun\/papers\/verif_ifm_with_pvs.ps"},{"key":"12_CR36","first-page":"437","volume-title":"Proc. of the 1st International Conference on Integrated Formal Methods (IFM 1999)","author":"H. Treharne","year":"1999","unstructured":"Treharne, H., Schneider, S.: Using a Process Algebra to Control B OPERATIONS. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proc. of the 1st International Conference on Integrated Formal Methods (IFM 1999), UK, pp. 437\u2013457. Springer, Heidelberg (1999)"},{"key":"12_CR37","first-page":"109","volume-title":"Proc. of the 1st Conference on Integrated Formal Methods (IFM 1999)","author":"J. Pol van de","year":"1999","unstructured":"van de Pol, J., Hooman, J., de Jong, E.: Modular Formal Specification of Data and Behaviour. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proc. of the 1st Conference on Integrated Formal Methods (IFM 1999), UK, pp. 109\u2013128. Springer, Heidelberg (1999)"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J. Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:49:44Z","timestamp":1553320184000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}