Autor:
Gallardo, María del Mar

Foto de perfil
E-mails conocidos
mdgallardo@uma.es
gallardo@lcc.uma.e
gallardo@lcc.uma.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Gallardo
Nombre de pila
María del Mar
Nombre
Nombres alternativos
Gallardo, Maria-Del-Mar
Gallardo, María-Del-Mar
Gallardo, Maria del Mar
Afiliaciones conocidas
Universidad de Málaga, Andalucía Tech, Dept. de Ciencias de la Computación
LCC, Universidad de Málaga
ITIS Software, University of Malaga, Spain
University of Málaga, Spain
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 201932020 - 20231
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 4 de 4
  • Miniatura
    Artículo
    An Event-driven Interval Temporal Logic for Hybrid Systems
    Gallardo, María del Mar; Panizo, 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
    xeLTL: Extending eLTL with variables
    Panizo, Laura; Gallardo, 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
    A discretized operational semantics for the implementation of Hy-tccp
    Gallardo, María del Mar; Panizo, 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, María del Mar; Panizo, 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.