Mostrar el registro sencillo del ítem

A formal library of set relations and its application to synchronous languages

dc.contributor.authorRocha, Camilo
dc.contributor.authorMuñoz, César
dc.contributor.authorDowek, Gilles
dc.date.accessioned2021-12-03T18:31:03Z
dc.date.available2021-12-03T18:31:03Z
dc.date.issued2011
dc.identifier.issn03043975
dc.identifier.urihttps://repositorio.escuelaing.edu.co/handle/001/1900
dc.description.abstractSet relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.eng
dc.description.abstractSet relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.spa
dc.format.extent14 páginas.spa
dc.format.mimetypeapplication/pdfspa
dc.language.isoengspa
dc.publisherElsevier B.V.spa
dc.titleA formal library of set relations and its application to synchronous languageseng
dc.typeArtículo de revistaspa
dc.type.versioninfo:eu-repo/semantics/publishedVersionspa
oaire.accessrightshttp://purl.org/coar/access_right/c_14cbspa
oaire.versionhttp://purl.org/coar/version/c_970fb48d4fbd8a85spa
dc.contributor.researchgroupInformáticaspa
dc.relation.citationendpage4866spa
dc.relation.citationissue37spa
dc.relation.citationstartpage4853spa
dc.relation.citationvolume412spa
dc.relation.indexedN/Aspa
dc.relation.ispartofjournalTheoretical Computer Scienceeng
dc.relation.referencesM. AlTurki, J. Meseguer, Reduction semantics and formal analysis of Orc programs, Electr. Notes Theor. Comput. Sci. 200 (3) (2008) 25–41.spa
dc.relation.referencesF. Baader, T. Nipkow, Term Rewriting and all that, Cambridge University Press, Cambridge, 1998.spa
dc.relation.referencesJ.-P. Banâtre, D.L. Métayer, The GAMMA model and its discipline of programming, Science of Computer Programming 15 (1) (1990) 55–77.spa
dc.relation.referencesG. Berry, The foundations of Esterel, in: Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, MA, USA, 2000, pp. 425–454.spa
dc.relation.referencesG. Berry, G. Boudol, The chemical abstract machine, Theoretical Computer Science 96 (1) (1992) 217–248.spa
dc.relation.referencesP. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice, Lustre: a declarative language for real-time programming, in: POPL’87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages, ACM, New York, NY, USA, 1987, pp. 178–188.spa
dc.relation.referencesM. Clavel, F. Durán, S. Eker, J. Meseguer, P. Lincoln, N. Martí-Oliet, C. Talcott, All About Maude — A High-Performance Logical Framework, 1st ed., in: LNCS, vol. 4350, Springer, 2007.spa
dc.relation.referencesS. Dajani-Brown, D. Cofer, A. Bouali, Formal verification of an avionics sensor voter using SCADE, in: Y. Lakhnech, S. Yovine (Eds.), FORMATS/FTRTFT, in: Lecture Notes in Computer Science, vol. 3253, Springer, 2004, pp. 5–20.spa
dc.relation.referencesR. De Simone, A. Ressouche, Compositional semantics of Esterel and verification by compositional reductions, Lecture Notes in Computer Science 818 (1994) 441–454.spa
dc.relation.referencesN. Dershowitz, J.P. Jouannaud, Rewrite systems, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), The MIT Press, 1990, pp. 243–320.spa
dc.relation.referencesG. Dowek, C. Muñoz, C. Păsăreanu, A formal analysis framework for PLEXIL, in: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems, September 2007, pp. 45–51.spa
dc.relation.referencesG. Dowek, C. Muñoz, C. Păsăreanu, A small-step semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.spa
dc.relation.referencesG. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, CoRR abs/1002.2872, 2010.spa
dc.relation.referencesT. Estlin, A. Jónsson, C. Păsăreanu, R. Simmons, K. Tso, V. Verna, Plan Execution Interchange Language (PLEXIL), Technical Memorandum TM-2006- 213483, NASA, 2006.spa
dc.relation.referencesP.L. Guernic, T. Gautier, M.L. Borgne, C.L. Maire, Programming real-time applications with SIGNAL, Proceedings of the IEEE 79 (9) (1991) 1321–1336.spa
dc.relation.referencesK. Harbusch, P. Poller, Structural translation with synchronous rewriting systems, Technical Report RT-94-01, Université Paris 7, Paris, France, 1994.spa
dc.relation.referencesD. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming 8 (3) (1987) 231–274.spa
dc.relation.referencesK. Heninger, Specifying software requirements for complex systems: new techniques and their application, IEEE Transactions on Software Engineering 6 (1) (1980) 2–13.spa
dc.relation.referencesD. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, Electronic Notes in Theoretical Computer Science 237 (2009) 107–125.spa
dc.relation.referencesG. Lüttgen, M. Beeck, R. Cleaveland, A compositional approach to statecharts semantics, in: ACM SIGSOFT 8th Intl. Symposium on Foundations of Software Engineering (FSE 2000), in: ACM Software Engineering Notes, vols. 25, 6, ACM Press, San Diego, California, November 2000, pp. 120–129.spa
dc.relation.referencesG. Lüttgen, M. Mendler, Axiomatizing an algebra of step reactions for synchronous languages, in: L. Brim, P. Jancar, M. Kretínský, A. Kucera (Eds.), CONCUR, in: Lecture Notes in Computer Science, vol. 2421, Springer, 2002, pp. 386–401.spa
dc.relation.referencesJ. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science 96 (1) (1992) 73–155.spa
dc.relation.referencesJ. Meseguer, Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems, in: S.F. Smith, C.L. Talcott (Eds.), FMOODS, in: IFIP Conference Proceedings, vol. 177, Kluwer, 2000, p. 89.spa
dc.relation.referencesJ. Meseguer, G. Rosu, The rewriting logic semantics project, Theoretical Computer Science 373 (3) (2007) 213–237.spa
dc.relation.referencesR. Owen, S. Giorgio, Synchronous models of language, in: Proceedings of the 34th annual meeting on Association for Computational Linguistics, Association for Computational Linguistics, Morristown, NJ, USA, 1996, pp. 116–123.spa
dc.relation.referencesS. Owre, J. Rushby, N. Shankar, PVS: a prototype verification system, in: D. Kapur (Ed.), 11th International Conference on Automated Deduction (CADE), in: Lecture Notes in Artificial Intelligence, vol. 607, Springer-Verlag, Saratoga, NY, June 1992, pp. 748–752.spa
dc.relation.referencesG.D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60–61 (2004) 17–139.spa
dc.relation.referencesP. Sampath, A.C. Rajeev, S. Ramesh, K.C. Shashidhar, Testing model-processing tools for embedded systems, in: IEEE Real-Time and Embedded Technology and Applications Symposium, IEEE Computer Society, 2007, pp. 203–214.spa
dc.relation.referencesT. Serbanuta, G. Stefanescu, G. Rosu, Defining and executing P systems with structured data in k, in: D.W. Corne, P. Frisco, G. Paun, G. Rozenberg, A. Salomaa (Eds.), Workshop on Membrane Computing, in: Lecture Notes in Computer Science, vol. 5391, Springer, 2008, pp. 374–393.spa
dc.relation.referencesO. Tardieu, A deterministic logical semantics for pure esterel, ACM Transactions on Programming Languages and Systems 29 (2) (2007) 8.spa
dc.relation.referencesP. Viry, Equational rules for rewriting logic, Theoretical Computer Science 285 (2002) 487–517.spa
dc.rights.accessrightsinfo:eu-repo/semantics/closedAccessspa
dc.subject.armarcEstablecer relacionesspa
dc.subject.armarcSynchronous languagesspa
dc.subject.armarcSemántica de pasos pequeñosspa
dc.subject.armarcSemántica lógicaspa
dc.subject.armarcEjecución del planspa
dc.subject.proposalSet relationseng
dc.subject.proposalLenguajes síncronosspa
dc.subject.proposalSmall-step semanticseng
dc.subject.proposalRewriting logic semanticseng
dc.subject.proposalPlan executioneng
dc.type.coarhttp://purl.org/coar/resource_type/c_6501spa
dc.type.contentTextspa
dc.type.driverinfo:eu-repo/semantics/articlespa
dc.type.redcolhttp://purl.org/redcol/resource_type/ARTspa


Ficheros en el ítem

Thumbnail
Nombre:
A formal library of set relations ...
Tamaño:
372.2Kb
Formato:
PDF
Descripción:
Artículo de revista
Ver/

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem