Patents

PATENTS

  • Patent Title :  CALPE: Calculation of Catenary Pins
    Inventors/authors/obtainers : Tomás Rojo, Enrique Arias, Jesús Benet, David Cebrian, Fernando Cuartero, Jesús Montesinos, Pedro Tendero, Angelines Alberto
    N. of registry seat : 00/2008/1524
    Registration in the OEPM : M2808488-8
  • Patent Title :  InDiCa: Pantograph / Catenary Dynamic Interaction
    Inventors/authors/obtainers : Tomás Rojo, Enrique Arias, Jesús Benet, David Cebrian, Fernando Cuartero, Jesús Montesinos, Pedro Tendero, Angelines Alberto
    N. of registry seat : 00/2008/1525
    Registration in the OEPM : M2802874-0
  • Patent Title :  InDiCa2: Pantograph / Catenary Dynamic Interaction
    Inventors/authors/obtainers : Tomás Rojo, Enrique Arias, Jesús Benet, Fernando Cuartero, Jesús Montesinos, Pedro Tendero, Alejandro Jiménez, Nuria Cuartero
    Registration number : AB-92-2014
    Registration in the OEPM :
  • Patent Title : InDiCa3: Dynamic Interaction Pantograph / Catenary in 3 Dimensions
    Inventors/authors/obtainers : Tomás Rojo, Enrique Arias, Jesús Benet, Fernando Cuartero, Jesús Montesinos, Pedro Tendero, Alejandro Jiménez, Nuria Cuartero
    Registration number : AB-92-2014
    Registration in the OEPM :
  • Patent Title : CALPE 7 : Calculation of Catenaria Pendolas, Version 7.
    Inventors/authors/obtainers : Tomás Rojo, Enrique Arias, Jesús Benet, Fernando Cuartero, Jesús Montesinos, Pedro Tendero, Alejandro Jiménez, Nuria Cuartero
    Registration number : AB-92-2014
    Registration in the OEPM :

Our group is developing two tools which can be used in computer aided verification

Learn More

TPAL tool

TPAL is a tool for the verification and simulation of concurrent systems, which are modeled by using a Timed and Probabilistic Process Algebra. The main advantage of TPAL is that we may write the specifications directly by using an algebraic language, and some alternative representation can automatically generated. The current version of TPAL has the following features:

Full support for the creation and edition of specifications and projects in TPAL. Syntax and semantic analysis of TPAL specifications. Generation of Probabilistic-Dynamic State Graphs for TPAL specifications. Simple reduction of the generated graphs. Graph browser, and simulation by using the graphs. Generation of Timed-Arc Petri Nets. Timed-Arc Petri Nets browser, and simulation by using the nets. Translation of Dynamic State Graphs into Time Automata for UPPAAL tool. Configuration of some parameters (graph browser and simulation.)

You can obtain the current linux version HERE.