A discretized operational semantics for the implementation of Hy-tccp

Resumen:

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.

Palabras Clave:

Autor(es):

• María del Mar Gallardo {gallardo@lcc.uma.es}
  Dept. Lenguajes y Ciencias de la Computación E.T.S.I. Informatica University of Málaga
  
• Laura Panizo {laurapanizo@lcc.uma.es}
  Dept. Lenguajes y Ciencias de la Computación E.T.S.I. Informatica University of Málaga
  
• Laura Titolo {laura.titolo@lcc.uma.es}
  Dept. Lenguajes y Ciencias de la Computación E.T.S.I. Informatica University of Málaga
  

Handle:

Descargas:

La descarga de este artículo ha sido restringida por el autor

Ver la referencia en formato Bibtex