Listar AD - CTG – Informática por autor "ebfd407af468605647a49186059da397"

Mostrando ítems 1-7 de 7

    • Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories 

      Rocha, Camilo; Meseguer, José (SpringerBerlín, 2010)
      Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...

    • A Formal Interactive Verification Environment for the Plan Execution Interchange Language 

      Cadavid Rengifo, Hector Fabio; Rocha, Camilo; Muñoz, Cesar (Springer NatureUSA.Switzerland, 2012)
      The 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 ...

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

      Rocha, Camilo; Muñoz, César; Dowek, Gilles (Elsevier B.V., 2011)
      Set 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 ...

    • A Graphical Environment for the Semantic Validation of a Plan Execution Language 

      Rocha, Camilo; Muñoz, Cesar; Cadavid, Hector (© Copyright 2021 IEEEUSA., 2009)
      This paper presents PLEXIL5, PLEXIL's formal interacting visual environment, a graphical environment providing an user-friendly interface to the formal operational semantics of PLEXIL. PLEXIL is a synchronous plan execution ...

    • Rewriting Logic Semantics of a Plan Execution Language 

      Dowek, Gilles; Muñoz, César; Rocha, Camilo (E.E.U.U., 2010)
      The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a ...

    • Simulation and Verification of Synchronous Set Relations in Rewriting Logic 

      Rocha, Camilo; Múñoz, César (NASA Langley Research CenterHampton, Virginia., 2011)
      This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract ...

    • Tool Interoperability in the Maude Formal Environment 

      Durán, Francisco; Rocha, Camilo; Álvarez, José María (SpringerBerlín, 2011)
      We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the ...