Autor:
Panizo Jaime, Laura

Foto de perfil

E-mails conocidos

laurapanizo@uma.es
laurapanizo@lcc.uma.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Panizo Jaime

Nombre de pila

Laura

Nombre

Nombres alternativos

Panizo, Laura

Afiliaciones conocidas

Universidad de Málaga, Andalucía Tech, Dept. de Ciencias de la Computación
ITIS Software, University of Malaga, Spain
University of Málaga, Spain
ITIS Software, Universidad de Málaga, Spain

Páginas web conocidas

http://www.morse.uma.es/user/20
Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 201932020 - 20242
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 5 de 5
  • Miniatura
    Artículo
    An Event-driven Interval Temporal Logic for Hybrid Systems
    Gallardo Melgarejo, María del Mar; Panizo Jaime, Laura. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    Nowadays, hybrid systems are present in many crucial tasks of our daily life. The hybrid character derives from the merge of continuous and discrete dynamics that are intrinsically related. The verification of critical properties of hybrid systems is of special importance, but sometimes it is not feasible due to their inherent complexity. In the last few years, several model-based testing and runtime verification techniques have been proposed to support the verification and validation of hybrid systems. In this paper, we present an interval logic that is suitable for specifying properties of event-driven hybrid systems. We introduce the syntax and semantics of the logic, and propose an automatic mechanism to transform each logic formula into a network of timed automata that can act as observers of the property in each test case using the UPPAAL tool.
  • Miniatura
    Artículo
    A discretized operational semantics for the implementation of Hy-tccp
    Gallardo Melgarejo, María del Mar; Panizo Jaime, Laura; Titolo, Laura. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    The language Hy-tccp was proposed as an extension of the Timed Concurrent Constraint paradigm (tccp) with continuous time and suitable mechanisms to handle continuous behaviors. This language provides a powerful model for hybrid and cyber-physical systems including concurrency and syn chronization features. In this paper, we propose a discretized operational semantics for Hy-tccp and an extension of the standard LTL to reason about temporal properties of Hy-tccp programs. The semantics and the logics will be the basis for the definition of formal verification and analysis tools, such as model checkers and theorem provers.
  • Miniatura
    Artículo
    Modelling and Specifying Software Systems with Alloy
    Gallardo Melgarejo, María del Mar; Panizo Jaime, Laura. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.
    Alloy is both a modelling and specifying language of software systems, and a tool to automatically check the consistency of descriptions. Alloy uses sets and set relations to describe the high-level structure of systems, and a first-order relational logic to enrich models with more specific properties. A similar methodology is followed by software engineers when using OCL to complete the UML descriptions with more detailed features that improve the specifications. Alloy is able to construct and analyze the consistency of static specifications of complex systems, producing snapshots of possible model instances. In addition, Alloy can also describe dynamic specifications that show how the system may evolve over time when executing transitions. In this tutorial, we present the main features of the language and illustrate them by means of an example consisting in the specification and modelling of Software-Defined Networks. The example is sufficiently complex to permit the use of the most significant Alloy constructors.
  • Miniatura
    Artículo
    xeLTL: Extending eLTL with variables
    Panizo Jaime, Laura; Gallardo Melgarejo, María del Mar. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    Our daily activity is increasingly integrated with systems that somehow adapt their behaviour to our state or reactions. These systems are usually called reactive systems since they evolve based on internal or external events produced by their environment. The massive use of smartphones and wearable devices for health monitoring is just an example of how these systems impact in our lives. In addition, some systems, such as those for assisted or autonomous driving, carry out critical tasks. Thus, it is important to ensure that reactive systems satisfy safety requirements in which, in many cases, is relevant the evolution of time or other physical magnitudes. In this paper, we present the eXtended Event-driven Temporal Logic (xeLTL) that can express requirements over intervals of parameterized events.
  • Miniatura
    Artículo
    LearnTA: Generación automática de autómatas temporizados mediante el aprendizaje de trazas
    López Gómez, Rafael; Panizo Jaime, Laura; Gallardo Melgarejo, María del Mar. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.
    El rápido avance de tecnologías, como la Inteligencia Artificial, está permitiendo el desarrollo de sistemas software muy sofisticados. Para la detección temprana de errores en estos sistemas es usual la construcción de modelos abstractos sobre los que se pueda razonar. Sin embargo, esta tarea de modelado se complica cuando lo ́único que puede observarse de los sistemas es su interacción con el entorno. En este trabajo, se presenta LearnTA, una herramienta de aprendizaje para la generación automática de modelos de sistemas (Systems Under Learning/SULs) a partir de la observación de su ejecución. Concretamente, la herramienta tiene como objetivo aprender sistemas reactivos cuya evolución puede depender del tiempo. LearnTA emplea un algoritmo de Automata Learning con aprendizaje pasivo. LearnTA utiliza el comportamiento observado del SUL que se quiere aprender para construir un modelo formal. El comportamiento observado del SUL está constituido por secuencias (trazas) de observaciones, cada una de las cuales tiene un evento de interacción del sistema con su entorno y su estado visible en un instante de tiempo. El modelo formal construido por LearnTA es un tipo especial de autómata de tiempo real determinista. Para evaluar LearnTA, se han realizado una serie de experimentos en los que los SULs son sistemas sintéticos de diferente tamaño. Asimismo, también se ha realizado una comparación con TAG, otro herramienta perteneciente al estado del arte.