- -

Listar por palabra clave "Model checking"

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Listar por palabra clave "Model checking"

Ordenar por:Orden:Resultados:

  • thumb
    A Model-Driven CASE tool for developing and verifying regulated open MAS 
    Garcia Marques, Mª Emilia; Giret Boggino, Adriana Susana; Botti, V. (Elsevier, 2013-06)
    [EN] This paper describes a CASE tool for developing complex systems in which heterogeneous and autonomous agents may need to coexist in a complex social and legal framework. Model-Driven Technologies are used to integrate ...
  • thumb
    A rewriting logic approach to the formal specification and verification of web applications 
    Alpuente Frasnedo, María; Ballis, Demis; Romero, Daniel Omar (Elsevier, 2014-02-15)
    [EN] This paper develops a Rewriting Logic framework for the automatic specification and verification of Web applications that considers the critical aspects of concurrent Web interactions, browser navigation features ...
  • thumb
    A sufficient condition to polynomially compute a minimum separating DFA 
    Vázquez-De-Parga Andrade, Manuel; García Gómez, Pedro; López Rodríguez, Damián (Elsevier, 2016-11-20)
    The computation of a minimal separating automaton (MSA) for regular languages has been studied from many different points of view, from synthesis of automata or Grammatical Inference to the minimization of incompletely ...
  • thumb
    AMC - Tool support for automating Model Checking Lifecycle 
    López Pons, Luis Enrique (Universitat Politècnica de València, 2013-04-29)
    In model checking, the most time consuming stage is oftentimes not writing the formal model (of the system to be analyzed) itself but validating the model: ensuring the correct system has been modeled, before ensuring ...
  • thumb
    Datalog-Based program analysis with BES and RWL 
    Alpuente Frasnedo, María; Feliú Gabaldón, Marco Antonio; Joubert, Christophe; Villanueva García, Alicia (Springer Verlag (Germany), 2011)
    This paper describes two techniques for Datalog query evaluation and their application to object-oriented program analysis. The first technique transforms Datalog programs into an implicit Boolean Equation System (Bes) ...
  • thumb
    Engineering regulated open multiagent systems 
    Garcia Marques, Mª Emilia (IOS Press, 2014)
    In this thesis, w e focus on the d e velopment o f normati v e open multiagent systems. The y are systems in which heterogeneous and autonomous agents may need to coexist in a complex social and legal framework ...
  • thumb
    Modelado y verificación del protocolo de exclusión mutua con tiempo real Fischer usando Maude 
    García Valero, Víctor (Universitat Politècnica de València, 2021-09-15)
    [ES] En el siguiente trabajo modelamos el protocolo de exclusión mutua con tiempo real Fischer como un módulo de sistema mediante el lenguaje de especificación y verificación Maude. Hacemos uso del alcance de la generación ...
  • thumb
    Passage retrieval in legal texts 
    Rosso, Paolo; Correa García, Santiago; Buscaldi, Davide (Elsevier, 2011-07)
    [EN] Legal texts usually comprise many kinds of texts, such as contracts, patents and treaties. These texts usually include a huge quantity of unstructured information written in natural language. Thanks to automatic ...
  • thumb
    Towards Symbolic Execution in Erlang 
    Vidal Oriola, Germán Francisco (Springer, 2015-04)
    The concurrent functional language Erlang [1] has a number of distinguishing features, like dynamic typing, concurrency via asynchronous message passing or hot code loading, that make it especially appropriate for ...
  • thumb
    Verificacion Automática del Comportamiento de un Robot Asistente 
    León Guerrero, Alejandro (Universitat Politècnica de València, 2019-09-09)
    [ES] Los asistentes robóticos autónomos están diseñados para ofrecer compañía a personas que viven en un ambiente doméstico. Este tipo de robot usa diversos sensores para detectar y adaptarse a cualquier imprevisto en el ...
  • thumb
    Verificación automática del protocolo TLS 1.3 usando Maude-NPA 
    Lluch Palop, José (Universitat Politècnica de València, 2019-10-30)
    [ES] La importancia de la confidencialidad y seguridad en las tecnologías de la información es un tema en el que poco a poco más entidades tanto públicas como privadas aúnan esfuerzos con el fin de conseguir entornos ...
  • thumb
    Verificación de aplicaciones web dinámicas con Web-TLR 
    Espert Real, Javier (Universitat Politècnica de València, 2011-07-20)
    Web-TLR is a software tool designed for model-checking Web applications that is based on rewriting logic. Web applications are expressed as rewrite theories that can be formally verified by using the Maude built-in LTLR ...