Show simple item record

dc.contributor.authorCadavid Rengifo, Hector Fabio
dc.contributor.authorRocha, Camilo
dc.contributor.authorMuñoz, Cesar
dc.description.abstractThe Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.eng
dc.description.abstractEl lenguaje de intercambio de ejecución de planes (PLEXIL) es un lenguaje síncrono de código abierto desarrollado por la NASA para controlar y monitorear sistemas autónomos. Este documento informa sobre el desarrollo del entorno de verificación interactivo formal de PLEXIL (PLEXIL5), una interfaz gráfica para la semántica ejecutable formal de PLEXIL. Entre sus principales características, PLEXIL5 proporciona verificación de modelos de planes con soporte para edición de fórmulas y visualización de contraejemplos, simulación interactiva de planes en diferentes niveles de granularidad e inicialización aleatoria de variables de entorno externo. Las capacidades de verificación formal de PLEXIL5 se ilustran mediante un modelo de interacción humano-automatizació
dc.format.extent15 pá
dc.publisherSpringer Naturespa
dc.relation.ispartofseriesLNCS;Volumen 7321
dc.rights© Springer Nature Switzerland AG 2018eng
dc.titleA Formal Interactive Verification Environment for the Plan Execution Interchange Languageeng
dc.typeCapítulo - Parte de Librospa
dc.relation.ispartofbookLecture Notes in Computer Scienceeng
dc.relation.referencesBalasubramanian, D., Păsăreanu, C., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple Statechart formalisms. In: Dwyer, M.B., Tip, F. (eds.) ISSTA, pp. 45–55. ACM (2011)spa
dc.relation.referencesBolton, M.L., Bass, E.J., Siminiceanu, R.I.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Transactions on Systems, Man, and Cybernetics–Part A: Systems and Humans 41(5), 961–976 (2011)spa
dc.relation.referencesBruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)spa
dc.relation.referencesClavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)spa
dc.relation.referencesDowek, G., Muñoz, C., Păsăreanu, C.: A small-step semantics of PLEXIL. Technical Report 2008-11, National Institute of Aerospace, Hampton, VA (2008)spa
dc.relation.referencesDowek, G., Muñoz, C., Păsăreanu, C.: A formal analysis framework for PLEXIL. In: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems (September 2007)spa
dc.relation.referencesDowek, G., Muñoz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. In: Klin, B., Sobocinski, P. (eds.) SOS. EPTCS, vol. 18, pp. 77–91 (2009)spa
dc.relation.referencesEstlin, T., Jónsson, A., Păsăreanu, C., Simmons, R., Tso, K., Verma, V.: Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA (2006)spa
dc.relation.referencesMartí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electronic Notes in Theoretical Computer Science 238(3), 227–247 (2009)spa
dc.relation.referencesMeseguer, J.: Conditional rewriting logic as a united model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)spa
dc.relation.referencesRocha, C., Muñoz, C., Cadavid, H.: A graphical environment for the semantic validation of a plan execution language. In: IEEE International Conference on Space Mission Challenges for Information Technology, pp. 201–207. IEEE Computer Society, Los Alamitos (2009)spa
dc.relation.referencesRocha, C., Muñoz, C.: Simulation and Verification of Synchronous Set Relations in Rewriting Logic. In: da Silva Simão, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 60–75. Springer, Heidelberg (2011)spa
dc.relation.referencesRocha, C., Muñoz, C., Dowek, G.: A formal library of set relations and its application to synchronous languages. Theoretical Computer Science 412(37), 4853–4866 (2011)spa
dc.relation.referencesRosu, G., Serbanuta, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)spa
dc.relation.referencesSantiago, S., Talcott, C.L., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Electronic Notes in Theoretical Computer Science 258(1), 3–20 (2009)spa
dc.relation.referencesStrauss, P.J.: Executable semantics for PLEXIL: simulating a task-scheduling language in Haskell. Master’s thesis, Oregon State University (2009)spa
dc.relation.referencesVerdejo, A., Martí-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods in System Design 27(1-2), 113–172 (2005)spa
dc.relation.referencesVerma, V., Jónsson, A., Păsăreanu, C., Iatauro, M.: Universal Executive and PLEXIL: Engine and language for robust spacecraft control and operations. In: Proceedings of the American Institute of Aeronautics and Astronautics Space Conference (2006)spa
dc.rights.creativecommonsAtribución 4.0 Internacional (CC BY 4.0)spa
dc.subject.armarcComprobación del modelospa
dc.subject.armarcLógica Temporal Linealspa
dc.subject.armarcProposición atómicaspa
dc.subject.armarcLenguaje síncronospa
dc.subject.armarcEstructura Kripkespa
dc.subject.proposalModel Checkeng
dc.subject.proposalLinear Temporal Logiceng
dc.subject.proposalAtomic Propositioneng
dc.subject.proposalPlan Executioneng
dc.subject.proposalKripke Structureeng

Files in this item


This item appears in the following Collection(s)

Show simple item record

© Springer Nature Switzerland AG 2018
Except where otherwise noted, this item's license is described as © Springer Nature Switzerland AG 2018