Especificación de la red móvil mediante un enfoque formal similar a wp

El documento tiene como objetivo proporcionar un sistema formal, motivado por la condición previa más débil de Dijkstra lógica, para especificar la red móvil. El documento muestra cómo se puede especificar la movilidad utilizando un enfoque basado en el estado y la transición, que permite que los ho...

Full description

Autores:: Kumar Singh, Awadhesh
Ghanekar, Umesh
Bandyopadhyay, Anup Kumar

Tipo de recurso:: Trabajo de grado de pregrado

Fecha de publicación:: 2005

Institución:: Universidad Autónoma de Bucaramanga - UNAB

Repositorio:: Repositorio UNAB

Idioma:: spa

id	UNAB2_388efce4f66ef974b14bc4028787e7dc
oai_identifier_str	oai:repository.unab.edu.co:20.500.12749/9021
network_acronym_str	UNAB2
network_name_str	Repositorio UNAB
repository_id_str
dc.title.spa.fl_str_mv	Especificación de la red móvil mediante un enfoque formal similar a wp
dc.title.translated.eng.fl_str_mv	Specifying mobile network using a wp-like formal approach
title	Especificación de la red móvil mediante un enfoque formal similar a wp
spellingShingle	Especificación de la red móvil mediante un enfoque formal similar a wp Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Weakest precondition Mobile computing Specification verification Safety Handover Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones Condición previa más débil Computación móvil Especificación Verificación Seguridad Entregar
title_short	Especificación de la red móvil mediante un enfoque formal similar a wp
title_full	Especificación de la red móvil mediante un enfoque formal similar a wp
title_fullStr	Especificación de la red móvil mediante un enfoque formal similar a wp
title_full_unstemmed	Especificación de la red móvil mediante un enfoque formal similar a wp
title_sort	Especificación de la red móvil mediante un enfoque formal similar a wp
dc.creator.fl_str_mv	Kumar Singh, Awadhesh Ghanekar, Umesh Bandyopadhyay, Anup Kumar
dc.contributor.author.spa.fl_str_mv	Kumar Singh, Awadhesh Ghanekar, Umesh Bandyopadhyay, Anup Kumar
dc.contributor.orcid.spa.fl_str_mv	Anup Kumar Bandyopadhyay [0000-0002-0503-8441]
dc.subject.none.fl_str_mv	Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s
topic	Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Weakest precondition Mobile computing Specification verification Safety Handover Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones Condición previa más débil Computación móvil Especificación Verificación Seguridad Entregar
dc.subject.keywords.eng.fl_str_mv	Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Weakest precondition Mobile computing Specification verification Safety Handover
dc.subject.lemb.spa.fl_str_mv	Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones
dc.subject.proposal.spa.fl_str_mv	Condición previa más débil Computación móvil Especificación Verificación Seguridad Entregar
description	El documento tiene como objetivo proporcionar un sistema formal, motivado por la condición previa más débil de Dijkstra lógica, para especificar la red móvil. El documento muestra cómo se puede especificar la movilidad utilizando un enfoque basado en el estado y la transición, que permite que los hosts móviles sean tratados como nodos en un sistema distribuido estructurado estáticamente tradicional. Otro objetivo es razonar formalmente sobre la posibles comportamientos de un sistema formado por componentes móviles. El procedimiento de entrega sirve como una ilustración para la notación. La contribución del artículo es el desarrollo de un estilo de modelado y razonamiento sobre las propiedades temporales que permite una análisis exhaustivo de los sistemas móviles.
publishDate	2005
dc.date.issued.none.fl_str_mv	2005-12-01
dc.date.accessioned.none.fl_str_mv	2020-10-27T00:21:10Z
dc.date.available.none.fl_str_mv	2020-10-27T00:21:10Z
dc.type.coar.fl_str_mv	http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv	http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.driver.none.fl_str_mv	info:eu-repo/semantics/article
dc.type.local.spa.fl_str_mv	Artículo
dc.type.coar.none.fl_str_mv	http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.none.fl_str_mv	http://purl.org/redcol/resource_type/CJournalArticle
format	http://purl.org/coar/resource_type/c_7a1f
dc.identifier.issn.none.fl_str_mv	2539-2115 1657-2831
dc.identifier.uri.none.fl_str_mv	http://hdl.handle.net/20.500.12749/9021
dc.identifier.instname.spa.fl_str_mv	instname:Universidad Autónoma de Bucaramanga UNAB
dc.identifier.repourl.none.fl_str_mv	repourl:https://repository.unab.edu.co
identifier_str_mv	2539-2115 1657-2831 instname:Universidad Autónoma de Bucaramanga UNAB repourl:https://repository.unab.edu.co
url	http://hdl.handle.net/20.500.12749/9021
dc.language.iso.spa.fl_str_mv	spa
language	spa
dc.relation.none.fl_str_mv	https://revistas.unab.edu.co/index.php/rcc/article/view/1063/1035
dc.relation.uri.none.fl_str_mv	https://revistas.unab.edu.co/index.php/rcc/article/view/1063
dc.relation.references.none.fl_str_mv	R. M. B. E. Morsi and J. F. Leathrum. A formal specification and verification of GSM using the OSI-RM formal object model. In Proceedings of the Applied Telecommunication Symposium ATS’03, 30 March – 03 April, Orlando, Florida, pages 1– 6, 2003. L. Andriantsiferana, B. Ghribi and L. Logrippo. Prototyping and formal requirement validation of GPRS: a mobile data packet radio service for GSM. In Dependable Computing for Critical Application: Proceedings of the IEEE Conference, 6–8 January, pages 109–128, 1999. J. A. Hall, Seven myths of formal methods. IEEE Software, vol. 7, September, pages 11- 19, 1990. L. Lamport, Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2): 190–222, 1983. K. Finney, Mathematical notation in formal specification – too difficult for the masses?’. IEEE Transactions on Software Engineering, 22(2): 158-159, 1996 G. J. Doherty, J. F. Campos and M. D. Harrison, Representational reasoning and verification. Formal Aspects of Computing, 12(4): 260-277, 2000. W. H. Hesselink, Predicate transformers for recursive procedures with local variables. Formal Aspects of Computing, 11(6): 616-636, 1999. Z. Chaochen, C. A. R. Hoare and A. P. Raven, A calculus of durations. Information Processing Letters, 40(5): 269-276, 1991. M. Kirchner. Program verification with the mathematical soft-ware system Theorema. PhD thesis, Research Institute of Symbolic Computation, Linz, Austria, 1999. K. L. Ildiko. Program verification using Hoare logic. In Computer Aided Verification of Information Systems – A Practical Industry Oriented Approach: Proceedings of the Workshop CAVIS’03, 12th of February, e-Austria Institute, Timisoara, Romania, 2003. ]G. Smith. A formal framework for modeling and analyzing mobile systems. In Australasian Computer Science: Proceedings of the 27th ACM International Conference ACSC 2004, 26: 193–202, 2004. T. Imielinski and B. R. Badrinath, Mobile wireless computing: challenges in data management. Communications of the ACM, 37(10): 18–28, 1994. L. Lamport. Verification and specification of concurrent programs. In: J. W. de Bakker, W. –P. de Roever and G. Rozenberg (eds.), A Decade of Concurrency – Reflections and Perspectives: Proceedings of the REX Workshop, June, The Netherlands, SpringerVerlag, LNCS 803, pages 347–374, 1993. E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976. N. Popov. Verification using weakest precondition strategy. In Computer Aided Verification of Information Systems – A Practical Industry Oriented Approach: Proceedings of the Workshop CAVIS’03, 12th of February, e-Austria Institute, Timisoara, Romania, 2003. K. R. M. Leino. Efficient weakest preconditions. Technical Report MSR-TR-2004-34, April, Microsoft Research, 2004. M. Ben-Ari. Mathematical Logic for Computer Science. Prentice Hall, Englewood Cliffs, NJ, 1993. E. D’Hondt and P. Panangaden. Quantum weakest preconditions. In Quantum Programming Languages: Proceedings of the 2nd International Workshop QPL2004, 12– 13 July, Turku, Finland, pages 75–90, 2004. A. K. Singh and A. K. Bandyopadhyay, Verifying mutual exclusion and liveness properties with split preconditions. Journal of Computer Science and Technology, To appear, 2004. K. M. Chandi and B. A. Sanders, Predicate transformers for reasoning about concurrent computation. Science of Computer Programming, 24(2): 129–148, 1995. G. P. Pollini, Trends in hndover design. IEEE Communications Magazine, March, pages 82–90, 1996. R. Vijayan and J. M. Holtzman, A model for analyzing handoff algorithms. IEEE Transactions on Vehicular Technology, 42(3): 351–356, 1993. F. Graziosi, M. Pratesi, M. Ruggieri and F. Santucci, A multi-cell model of handover initiation in mobile cellular networks. IEEE Transactions on Vehicular Technology, 48(3): 802–814, 1999. S. Agarwal and J. M. Holtzman, Modelling and analysis of handoff algorithms in multicellular systems. In Proceedings of the IEEE Vehicular Technology Conference, pages 300–304, 1997. A. Aaroud, S. E. Labhalla and B. Bounabat. Design of GSM handover using MARDS model. In Information Technology and Applications: Proceedings of the 2nd International Conference ICITA2004, 9–11 January, Harbin, China, 2004. F. Orava and J. Parrow, An algebraic verification of a mobile network. Formal Aspects of Computing, 4(6): 497–543, 1992. T. Kapus and Z. Brezocnik. Verification of a mobile network in a shared-variables model. Presented at the Verifications in New Orientations’97 Workshop, May, Val Bregaglia, Switzerland, 1997. T. Kapus and Z. Brezocnik. TLA-style specification of a mobile network. In Proceedings of the 23rd EURUMICRO IEEE Conference EUROMICRO’97, 1–4 September, pages 440–447, 1997. T. Kapus and Z. Brezocnik. Verification of a mobile network handover procedure using Murφ. In Proceedings of the 6th Electro technical and Computer Science Conference ERK’97, Z. A. J. C. Baldomir (ed.), 25–27 September, Portoro~, Slovenia, pages A/83– 86, 1997. W. H. Hesselink, An assertional criterion for atomicity. Acta Informatica, 38(5): 343–366, 2002. L. Lamport, Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3): 155–495, 1982. M. Charpentier. An approach to composition motivated by wp. In Fundamental Approaches to Software Engineering: Proceedings of the 5th International Conference FASE’2002, April, Springer-Verlag, LNCS 2306, pages 1–14, 2002. N. H. Minsky, Y. M. Minsky and V. Ungureanu. Making tuple spaces safe for heterogeneous distributed systems. In Applied Computing – Special Track on Coordination Models, Languages and Applications: Proceedings of the ACM Symposium ACMSAC’2000, 19–21 April, Como, Italy, pages 218–226, 2000. L. Chunlin and L. Layuan. An agent-based approach for grid computing. In Parallel and Distributed Computing Applications and Technologies: Proceedings of the 4th International Conference PDCAT’2003, 27–29 August, pages 608–611, 2003. L. Lamport, A simple approach to specifying concurrent systems. Communications of the ACM, 32(1): 32–45, 1989. J. V. Guttag and J. J. Horning. Formal specification as a design tool. In Principles of Programming Languages: Proceedings of the ACM Symposium, January, Las Vegas, pages 251–261, 1980 L. Lamport. What it means for a concurrent program to specify a specification: why no one has specified priority. In Principles of Programming Languages: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium, January, New Orleans, pages 78–83, 1985. K. Sabnani, An algorithmic technique for protocol verification. IEEE Transaction on Communication, 36(8): 924–931, 1988. P. Wolper. Specifying interesting properties of programs in prepositional temporal logic. In Principles of Programming Languages: Proceedings of the 13th ACM Symposium, pages 184–193, 1986. L. Lamport. “Sometime” is sometimes “not never”: On the temporal logic of programs. In Principles of Programming Languages: Proceedings of the 7th Annual ACM Symposium, 28–30 January, Las Vegas, pages 174–185, 1980. E. A. Emerson. Temporal and modal logic. In: J. v. Leeuwen (ed.), Handbook of Theoretical Computer Science, vol. B, chapter 16, Elsevier Science, pages 995–1072, 1990. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer–Verlag, New York, 1992. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. SpringerVerlag, New York, 1995. E. M. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press, 1999. ]B. Bérard et al. Systems and Soft-ware Verification: Model-Checking Techniques and Tools. Springer–Verlag, New York, 2001. F. Laroussinie, N. Markey and P. Schnoebelen. Temporal logic with forgettable past. In Logic in Computer Science: Proceedings of the 17 Annual IEEE Symposium LICS'2002, 22–25 July th , Copenhagen, Denmark, pages 383–392, 2002. F. Laroussinie, N. Markey and P. Schnoebelen. Temporal logic with forgettable past. In Logic in Computer Science: Proceedings of the 17 Annual IEEE Symposium LICS'2002, 22–25 July th , Copenhagen, Denmark, pages 383–392, 2002. H. Dierks, Comparing model checking and logical reasoning for real-time systems. Formal Aspects of Computing, 16(2): 104–120, 2004.
dc.rights.none.fl_str_mv	Derechos de autor 2005 Revista Colombiana de Computación
dc.rights.coar.fl_str_mv	http://purl.org/coar/access_right/c_abf2
dc.rights.uri.*.fl_str_mv	http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.uri.none.fl_str_mv	http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.creativecommons.*.fl_str_mv	Atribución-NoComercial-SinDerivadas 2.5 Colombia
rights_invalid_str_mv	Derechos de autor 2005 Revista Colombiana de Computación http://creativecommons.org/licenses/by-nc-sa/4.0/ http://creativecommons.org/licenses/by-nc-nd/2.5/co/ Atribución-NoComercial-SinDerivadas 2.5 Colombia http://purl.org/coar/access_right/c_abf2
dc.format.mimetype.spa.fl_str_mv	application/pdf
dc.publisher.none.fl_str_mv	Universidad Autónoma de Bucaramanga UNAB
publisher.none.fl_str_mv	Universidad Autónoma de Bucaramanga UNAB
dc.source.none.fl_str_mv	Revista Colombiana de Computación; Vol. 6 Núm. 2 (2005): Revista Colombiana de Computación; 1-19
institution	Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv	https://repository.unab.edu.co/bitstream/20.500.12749/9021/1/2005_Articulo_Especificaci%c3%b3n%20de%20la%20red%20m%c3%b3vil%20mediante%20un%20enfoque%20formal%20similar%20a%20wp.pdf https://repository.unab.edu.co/bitstream/20.500.12749/9021/2/2005_Articulo_Especificaci%c3%b3n%20de%20la%20red%20m%c3%b3vil%20mediante%20un%20enfoque%20formal%20similar%20a%20wp.pdf.jpg
bitstream.checksum.fl_str_mv	f77d5646582e444faf0dcebefb8a53aa 088aa36a7a6102232e634b8a2369eeb6
bitstream.checksumAlgorithm.fl_str_mv	MD5 MD5
repository.name.fl_str_mv	Repositorio Institucional \| Universidad Autónoma de Bucaramanga - UNAB
repository.mail.fl_str_mv	repositorio@unab.edu.co
_version_	1814277688193449984
spelling	Kumar Singh, Awadheshacdac2db-4c60-45af-b823-785e95c70c9fGhanekar, Umeshe3028e5f-91af-42a7-adc0-7b5246dd46d6Bandyopadhyay, Anup Kumar340c0907-c133-4234-8c9b-07b4d0945f38Anup Kumar Bandyopadhyay [0000-0002-0503-8441]2020-10-27T00:21:10Z2020-10-27T00:21:10Z2005-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/9021instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coEl documento tiene como objetivo proporcionar un sistema formal, motivado por la condición previa más débil de Dijkstra lógica, para especificar la red móvil. El documento muestra cómo se puede especificar la movilidad utilizando un enfoque basado en el estado y la transición, que permite que los hosts móviles sean tratados como nodos en un sistema distribuido estructurado estáticamente tradicional. Otro objetivo es razonar formalmente sobre la posibles comportamientos de un sistema formado por componentes móviles. El procedimiento de entrega sirve como una ilustración para la notación. La contribución del artículo es el desarrollo de un estilo de modelado y razonamiento sobre las propiedades temporales que permite una análisis exhaustivo de los sistemas móviles.The paper aims at providing a formal system, motivated by Dijkstra’s weakest precondition logic, for specifying mobile network. The paper shows how mobility can be specified using a state and transition based approach, which allows mobile hosts to be treated as nodes in a traditional statically structured distributed system. Another goal is to reason formally about the possible behaviors of a system consisting of mobile components. The handover procedure serves as an illustration for the notation. The contribution of the paper is the development of a style of modeling and reasoning about the temporal properties that allows for a straightforward and thorough analysis of mobile systems.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1063/1035https://revistas.unab.edu.co/index.php/rcc/article/view/1063R. M. B. E. Morsi and J. F. Leathrum. A formal specification and verification of GSM using the OSI-RM formal object model. In Proceedings of the Applied Telecommunication Symposium ATS’03, 30 March – 03 April, Orlando, Florida, pages 1– 6, 2003.L. Andriantsiferana, B. Ghribi and L. Logrippo. Prototyping and formal requirement validation of GPRS: a mobile data packet radio service for GSM. In Dependable Computing for Critical Application: Proceedings of the IEEE Conference, 6–8 January, pages 109–128, 1999.J. A. Hall, Seven myths of formal methods. IEEE Software, vol. 7, September, pages 11- 19, 1990.L. Lamport, Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2): 190–222, 1983.K. Finney, Mathematical notation in formal specification – too difficult for the masses?’. IEEE Transactions on Software Engineering, 22(2): 158-159, 1996G. J. Doherty, J. F. Campos and M. D. Harrison, Representational reasoning and verification. Formal Aspects of Computing, 12(4): 260-277, 2000.W. H. Hesselink, Predicate transformers for recursive procedures with local variables. Formal Aspects of Computing, 11(6): 616-636, 1999.Z. Chaochen, C. A. R. Hoare and A. P. Raven, A calculus of durations. Information Processing Letters, 40(5): 269-276, 1991.M. Kirchner. Program verification with the mathematical soft-ware system Theorema. PhD thesis, Research Institute of Symbolic Computation, Linz, Austria, 1999.K. L. Ildiko. Program verification using Hoare logic. In Computer Aided Verification of Information Systems – A Practical Industry Oriented Approach: Proceedings of the Workshop CAVIS’03, 12th of February, e-Austria Institute, Timisoara, Romania, 2003.]G. Smith. A formal framework for modeling and analyzing mobile systems. In Australasian Computer Science: Proceedings of the 27th ACM International Conference ACSC 2004, 26: 193–202, 2004.T. Imielinski and B. R. Badrinath, Mobile wireless computing: challenges in data management. Communications of the ACM, 37(10): 18–28, 1994.L. Lamport. Verification and specification of concurrent programs. In: J. W. de Bakker, W. –P. de Roever and G. Rozenberg (eds.), A Decade of Concurrency – Reflections and Perspectives: Proceedings of the REX Workshop, June, The Netherlands, SpringerVerlag, LNCS 803, pages 347–374, 1993.E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976.N. Popov. Verification using weakest precondition strategy. In Computer Aided Verification of Information Systems – A Practical Industry Oriented Approach: Proceedings of the Workshop CAVIS’03, 12th of February, e-Austria Institute, Timisoara, Romania, 2003.K. R. M. Leino. Efficient weakest preconditions. Technical Report MSR-TR-2004-34, April, Microsoft Research, 2004.M. Ben-Ari. Mathematical Logic for Computer Science. Prentice Hall, Englewood Cliffs, NJ, 1993.E. D’Hondt and P. Panangaden. Quantum weakest preconditions. In Quantum Programming Languages: Proceedings of the 2nd International Workshop QPL2004, 12– 13 July, Turku, Finland, pages 75–90, 2004.A. K. Singh and A. K. Bandyopadhyay, Verifying mutual exclusion and liveness properties with split preconditions. Journal of Computer Science and Technology, To appear, 2004.K. M. Chandi and B. A. Sanders, Predicate transformers for reasoning about concurrent computation. Science of Computer Programming, 24(2): 129–148, 1995.G. P. Pollini, Trends in hndover design. IEEE Communications Magazine, March, pages 82–90, 1996.R. Vijayan and J. M. Holtzman, A model for analyzing handoff algorithms. IEEE Transactions on Vehicular Technology, 42(3): 351–356, 1993.F. Graziosi, M. Pratesi, M. Ruggieri and F. Santucci, A multi-cell model of handover initiation in mobile cellular networks. IEEE Transactions on Vehicular Technology, 48(3): 802–814, 1999.S. Agarwal and J. M. Holtzman, Modelling and analysis of handoff algorithms in multicellular systems. In Proceedings of the IEEE Vehicular Technology Conference, pages 300–304, 1997.A. Aaroud, S. E. Labhalla and B. Bounabat. Design of GSM handover using MARDS model. In Information Technology and Applications: Proceedings of the 2nd International Conference ICITA2004, 9–11 January, Harbin, China, 2004.F. Orava and J. Parrow, An algebraic verification of a mobile network. Formal Aspects of Computing, 4(6): 497–543, 1992.T. Kapus and Z. Brezocnik. Verification of a mobile network in a shared-variables model. Presented at the Verifications in New Orientations’97 Workshop, May, Val Bregaglia, Switzerland, 1997.T. Kapus and Z. Brezocnik. TLA-style specification of a mobile network. In Proceedings of the 23rd EURUMICRO IEEE Conference EUROMICRO’97, 1–4 September, pages 440–447, 1997.T. Kapus and Z. Brezocnik. Verification of a mobile network handover procedure using Murφ. In Proceedings of the 6th Electro technical and Computer Science Conference ERK’97, Z. A. J. C. Baldomir (ed.), 25–27 September, Portoro~, Slovenia, pages A/83– 86, 1997.W. H. Hesselink, An assertional criterion for atomicity. Acta Informatica, 38(5): 343–366, 2002.L. Lamport, Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3): 155–495, 1982.M. Charpentier. An approach to composition motivated by wp. In Fundamental Approaches to Software Engineering: Proceedings of the 5th International Conference FASE’2002, April, Springer-Verlag, LNCS 2306, pages 1–14, 2002.N. H. Minsky, Y. M. Minsky and V. Ungureanu. Making tuple spaces safe for heterogeneous distributed systems. In Applied Computing – Special Track on Coordination Models, Languages and Applications: Proceedings of the ACM Symposium ACMSAC’2000, 19–21 April, Como, Italy, pages 218–226, 2000.L. Chunlin and L. Layuan. An agent-based approach for grid computing. In Parallel and Distributed Computing Applications and Technologies: Proceedings of the 4th International Conference PDCAT’2003, 27–29 August, pages 608–611, 2003.L. Lamport, A simple approach to specifying concurrent systems. Communications of the ACM, 32(1): 32–45, 1989.J. V. Guttag and J. J. Horning. Formal specification as a design tool. In Principles of Programming Languages: Proceedings of the ACM Symposium, January, Las Vegas, pages 251–261, 1980L. Lamport. What it means for a concurrent program to specify a specification: why no one has specified priority. In Principles of Programming Languages: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium, January, New Orleans, pages 78–83, 1985.K. Sabnani, An algorithmic technique for protocol verification. IEEE Transaction on Communication, 36(8): 924–931, 1988.P. Wolper. Specifying interesting properties of programs in prepositional temporal logic. In Principles of Programming Languages: Proceedings of the 13th ACM Symposium, pages 184–193, 1986.L. Lamport. “Sometime” is sometimes “not never”: On the temporal logic of programs. In Principles of Programming Languages: Proceedings of the 7th Annual ACM Symposium, 28–30 January, Las Vegas, pages 174–185, 1980.E. A. Emerson. Temporal and modal logic. In: J. v. Leeuwen (ed.), Handbook of Theoretical Computer Science, vol. B, chapter 16, Elsevier Science, pages 995–1072, 1990.Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer–Verlag, New York, 1992.Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. SpringerVerlag, New York, 1995.E. M. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press, 1999.]B. Bérard et al. Systems and Soft-ware Verification: Model-Checking Techniques and Tools. Springer–Verlag, New York, 2001.F. Laroussinie, N. Markey and P. Schnoebelen. Temporal logic with forgettable past. In Logic in Computer Science: Proceedings of the 17 Annual IEEE Symposium LICS'2002, 22–25 July th , Copenhagen, Denmark, pages 383–392, 2002.F. Laroussinie, N. Markey and P. Schnoebelen. Temporal logic with forgettable past. In Logic in Computer Science: Proceedings of the 17 Annual IEEE Symposium LICS'2002, 22–25 July th , Copenhagen, Denmark, pages 383–392, 2002.H. Dierks, Comparing model checking and logical reasoning for real-time systems. Formal Aspects of Computing, 16(2): 104–120, 2004.Derechos de autor 2005 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Atribución-NoComercial-SinDerivadas 2.5 Colombiahttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 6 Núm. 2 (2005): Revista Colombiana de Computación; 1-19Innovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesTIC´sTechnological innovationsComputer scienceTechnology developmentSystems engineeringInvestigationsInformation and communication technologiesICT'sWeakest preconditionMobile computingSpecification verificationSafetyHandoverInnovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesCondición previa más débilComputación móvilEspecificaciónVerificaciónSeguridadEntregarEspecificación de la red móvil mediante un enfoque formal similar a wpSpecifying mobile network using a wp-like formal approachinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticlehttp://purl.org/coar/version/c_970fb48d4fbd8a85ORIGINAL2005_Articulo_Especificación de la red móvil mediante un enfoque formal similar a wp.pdf2005_Articulo_Especificación de la red móvil mediante un enfoque formal similar a wp.pdfArtículoapplication/pdf312157https://repository.unab.edu.co/bitstream/20.500.12749/9021/1/2005_Articulo_Especificaci%c3%b3n%20de%20la%20red%20m%c3%b3vil%20mediante%20un%20enfoque%20formal%20similar%20a%20wp.pdff77d5646582e444faf0dcebefb8a53aaMD51open accessTHUMBNAIL2005_Articulo_Especificación de la red móvil mediante un enfoque formal similar a wp.pdf.jpg2005_Articulo_Especificación de la red móvil mediante un enfoque formal similar a wp.pdf.jpgIM Thumbnailimage/jpeg7919https://repository.unab.edu.co/bitstream/20.500.12749/9021/2/2005_Articulo_Especificaci%c3%b3n%20de%20la%20red%20m%c3%b3vil%20mediante%20un%20enfoque%20formal%20similar%20a%20wp.pdf.jpg088aa36a7a6102232e634b8a2369eeb6MD52open access20.500.12749/9021oai:repository.unab.edu.co:20.500.12749/90212023-01-10 22:00:30.685open accessRepositorio Institucional \| Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Especificación de la red móvil mediante un enfoque formal similar a wp

Publicaciones similares