Performance Issues of Deterministic and Adaptive Ghost-Packet Routers. - María del Carmen Carrión 001; Gregorio Díaz 001; María Blanca Caminero (ICPP, 2001)

Automatic verification of the TLS handshake protocol. - Gregorio Díaz 001; Fernando Cuartero; Valentín Valero Ruiz; Fernando L. Pelayo (SAC, 2004)

Obtaining Probabilistic Dynamic State Graphs for TPPAL Processes. - Juan José Pardo; Valentín Valero Ruiz; M. Carmen Ruiz; Fernando Cuartero; Gregorio Díaz 001 (Australian Software Engineering Conference, 2005)

Automatic Translation of WS-CDL Choreographies to Timed Automata. - Gregorio Díaz 001; Juan José Pardo; María-Emilia Cambronero; Valentín Valero; Fernando Cuartero (EPEW/WS-FM, 2005)

Application of Formal Methods to the Analysis of Web Services Security. - Llanos Tobarra; Diego Cazorla; Fernando Cuartero; Gregorio Díaz 001 (EPEW/WS-FM, 2005)

An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol. - Gregorio Díaz 001; Kim Guldstrand Larsen; Juan José Pardo; Fernando Cuartero; Valentín Valero (SAC, 2005)

Verification of Web Services with Timed Automata. - Gregorio Díaz 001; Juan José Pardo; María-Emilia Cambronero; Valentín Valero; Fernando Cuartero (WWV, 2005)

Automatic generation of Correct Web Services Choreographies and Orchestrations with Model Checking Techniques. - Gregorio Díaz 001; María-Emilia Cambronero; Juan José Pardo; Valentín Valero; Fernando Cuartero (AICT/ICIW, 2006)

RT-UML for modeling Real-Time Web Services. - María-Emilia Cambronero; Gregorio Díaz 001; Juan José Pardo; Valentín Valero Ruiz; Fernando L. Pelayo (SCW, 2006)

Analysis and Verification of Time Requirements Applied to the Web Services Composition. - Gregorio Díaz 001; María-Emilia Cambronero; Llanos Tobarra; Valentín Valero; Fernando Cuartero (WS-FM, 2006)

Does ROSA provide a good view of the Memorizing Process? - Maria L. Pelayo; Fernando L. Pelayo; Fernando Cuartero; Valentín Valero; Gregorio Díaz 001; Elena Nieto (IEEE ICCI, 2007)

Testing Time Goal-Driven Requirements with Model Checking Techniques. - Gregorio Díaz 001; Elena Navarro 001; María-Emilia Cambronero; Valentín Valero; Fernando Cuartero (ECBS, 2007)

Using UML Diagrams to Model Real-Time Web Services. - María-Emilia Cambronero; Gregorio Díaz 001; Juan José Pardo; Valentín Valero (ICIW, 2007)

Analysis of Web Services Secure Conversation with Formal Methods. - Llanos Tobarra; Diego Cazorla; Fernando Cuartero; Gregorio Díaz 001 (ICIW, 2007)

Model Checking Wireless Sensor Network Security Protocols: TinySec + LEAP. - Llanos Tobarra; Diego Cazorla; Fernando Cuartero; Gregorio Díaz 001; María-Emilia Cambronero (WSAN, 2007)

Using RT-UML for modelling web services. - María-Emilia Cambronero; Juan José Pardo; Gregorio Díaz 001; Valentín Valero (SAC, 2007)

Model Checking Techniques applied to the design of Web Services. - Gregorio Díaz 001; María-Emilia Cambronero; Juan José Pardo; Valentín Valero; Fernando Cuartero (CLEI Electron. J., 2007)

Enhancing the expressivity of PADL for specifying Web Services Architectures. - Gregorio Díaz 001; María-Emilia Cambronero; Llanos Tobarra; Valentín Valero Ruiz; Fernando L. Pelayo (TAMoCo, 2008)

Automatically Deriving Choreography-Conforming Systems of Services. - Gregorio Díaz 001; Ismael Rodríguez 001 (IEEE SCC, 2009)

Checking the Conformance of Orchestrations with Respect to Choreographies in Web Services: A Formal Approach. - Gregorio Díaz 001; Ismael Rodríguez 001 (FMOODS/FORTE, 2009)

A Comparative Study between WSCI, WS-CDL, and OWL-S. - María-Emilia Cambronero; Gregorio Díaz 001; Enrique Martínez; Valentín Valero (ICEBE, 2009)

Design and Verification of Web Services Compositions. - Enrique Martínez; María-Emilia Cambronero; Gregorio Díaz 001; Valentín Valero (ICIW, 2009)

Formal Study of Prioritized Service Compositions. - César Andrés; Gregorio Díaz 001; Enrique Martínez; Yaofeng Zhang (SITIS, 2009)

Time Ordering Architecture in SCA. - Enrique Martínez; Gregorio Díaz 001; Carmen Rosa Martínez; María-Emilia Cambronero; Valentín Valero Ruiz (TAMoCo, 2009)

A Petri net approach for the design and analysis of Web Services Choreographies. - Valentín Valero; María-Emilia Cambronero; Gregorio Díaz 001; Hermenegilda Macià (J. Log. Algebraic Methods Program., 2009)

A barred operational semantics for a subset of WS-CDL with time restrictions. - Valentín Valero; Gregorio Díaz 001; María-Emilia Cambronero; Hermenegilda Macià (J. Log. Algebraic Methods Program., 2009)

Model checking wireless sensor network security protocols: TinySec + LEAP + TinyPK. - Llanos Tobarra; Diego Cazorla; Fernando Cuartero; Gregorio Díaz 001; María-Emilia Cambronero (Telecommun. Syst., 2009)

A Model for Visual Specification of E-contracts. - Enrique Martínez; Gregorio Díaz 001; María-Emilia Cambronero; Gerardo Schneider (IEEE SCC, 2010)

Verification of real-time systems design. - María-Emilia Cambronero; Valentín Valero Ruiz; Gregorio Díaz 001 (Softw. Test. Verification Reliab., 2010)

Contractually Compliant Service Compositions. - Enrique Martínez; Gregorio Díaz 001; María-Emilia Cambronero (ICSOC, 2011)

DIEGO: A Tool for DerIving chorEoGraphy-cOnforming Web Service Systems. - Pablo Rabanal; José Antonio Mateo; Ismael Rodríguez 001; Gregorio Díaz 001 (ICWS, 2011)

An Operational Semantics of BPEL Orchestrations Integrating Web Services Resource Framework. - José Antonio Mateo; Valentín Valero; Gregorio Díaz 001 (WS-FM, 2011)

Timed Automata Semantics for Visual e-Contracts - Enrique Martínez; María-Emilia Cambronero; Gregorio Díaz 001; Gerardo Schneider (FLACOS, 2011)

Validation and verification of Web services choreographies by using timed automata. - María-Emilia Cambronero; Gregorio Díaz 001; Valentín Valero; Enrique Martínez (J. Log. Algebraic Methods Program., 2011)

BPEL-RF: A formal framework for BPEL orchestrations integrating distributed resources - José Antonio Mateo; Valentín Valero; Gregorio Díaz 001 (CoRR, 2012)

Conformance Verification of Normative Specifications using C-O Diagrams - Gregorio Díaz 001; Luis Llana; Valentín Valero Ruiz; José Antonio Mateo (FLACOS, 2012)

A centralized and a decentralized method to automatically derive choreography-conforming web service systems. - Ismael Rodríguez 001; Gregorio Díaz 001; Pablo Rabanal; José Antonio Mateo (J. Log. Algebraic Methods Program., 2012)

Improving the Automatic Derivation of Choreography-conforming Web Services Systems. - Pablo Rabanal; Ismael Rodríguez 001; José Antonio Mateo; Gregorio Díaz 001 (ICCS, 2012)

Transforming Web Services Choreographies with priorities and time constraints into prioritized-time colored Petri nets. - Valentín Valero Ruiz; Hermenegilda Macià; Juan José Pardo; María-Emilia Cambronero; Gregorio Díaz 001 (Sci. Comput. Program., 2012)

WST: a tool supporting timed composite Web Services Model transformation. - María-Emilia Cambronero; Gregorio Díaz 001; Enrique Martínez; Valentín Valero Ruiz; Llanos Tobarra (Simul., 2012)

Contract Compliance Monitoring of Web Services. - Gregorio Díaz 001; Luis Llana (ESOCC, 2013)

A Coloured Petri Net Approach to Model and Analyse Stateful Workflows Based on WS-BPEL and WSRF. - José Antonio Mateo; Valentín Valero Ruiz; Hermenegilda Macià; Gregorio Díaz 001 (SEFM Workshops, 2014)

Specification and Verification of NormativeTexts Using C-O Diagrams. - Gregorio Díaz 001; María-Emilia Cambronero; Enrique Martínez; Gerardo Schneider (IEEE Trans. Software Eng., 2014)

Colored Petri Net Modeling of the Publish/Subscribe Paradigm in the Context of Web Services Resources. - Valentín Valero; Hermenegilda Macià; Gregorio Díaz 001; María-Emilia Cambronero (FMICS, 2015)

Model-checking verification of publish-subscribe architectures in web service contexts. - Gregorio Díaz 001; María-Emilia Cambronero; Hermenegilda Macià; Valentín Valero Ruiz (SAC, 2015)

The Simulation Relation for Formal E-Contracts. - Luis Llana; María-Emilia Cambronero; Gregorio Díaz 001 (SOFSEM, 2016)

Complex Event Processing Modeling by Prioritized Colored Petri Nets. - Hermenegilda Macià; Valentín Valero; Gregorio Díaz 001; Juan Boubeta-Puig; Guadalupe Ortiz 001 (IEEE Access, 2016)

Intelligent Transportation System to Control Air Pollution in Cities Using Complex Event Processing and Colored Petri Nets. - Gregorio Díaz 001; Hermenegilda Macià; Valentín Valero; Fernando Cuartero (IWANN (2), 2017)

Data-aware automatic derivation of choreography-conforming systems of services. - Pablo Rabanal; José Antonio Mateo; Ismael Rodríguez 001; Gregorio Díaz 001 (Comput. Stand. Interfaces, 2017)

Timed Automata Modeling and Verification for Publish-Subscribe Structures Using Distributed Resources. - Valentín Valero; Gregorio Díaz 001; María-Emilia Cambronero (IEEE Trans. Software Eng., 2017)

Combining Fuzzy Logic and CEP Technology to Improve Air Quality in Cities. - Hermenegilda Macià; Gregorio Díaz 001; Juan Boubeta-Puig; Edelmira Valero; Valentín Valero (ICCS (5), 2019)

An Intelligent System Integrating CEP and Colored Petri Nets for Helping in Decision Making About Pollution Scenarios. - Gregorio Díaz 001; Enrique Brazález; Hermenegilda Macià; Juan Boubeta-Puig; Valentín Valero (IWANN (1), 2019)

MEdit4CEP-CPN: An approach for complex event processing modeling by prioritized colored petri nets. - Juan Boubeta-Puig; Gregorio Díaz 001; Hermenegilda Macià; Valentín Valero; Guadalupe Ortiz 001 (Inf. Syst., 2019)

Facilitating the Quantitative Analysis of Complex Events through a Computational Intelligence Model-Driven Tool. - Gregorio Díaz 001; Hermenegilda Macià; Valentín Valero; Juan Boubeta-Puig; Guadalupe Ortiz 001 (Sci. Program., 2019)

An Intelligent Transportation System to control air pollution and road traffic in cities integrating CEP and Colored Petri Nets. - Gregorio Díaz 001; Hermenegilda Macià; Valentín Valero; Juan Boubeta-Puig; Fernando Cuartero (Neural Comput. Appl., 2020)

SLA-Driven modeling and verifying cloud systems: A Bigraphical reactive systems-based approach. - Oussama Kamel; Allaoua Chaoui; Gregorio Díaz 001; Mohamed Gharzouli (Comput. Stand. Interfaces, 2021)

greenITS: a proposal to compute low-pollution routes. - Hermenegilda Macià; Gregorio Díaz 001; Valentín Valero; Edelmira Valero; Enrique Brazález; Juan Boubeta-Puig (FNC/MobiSPC/SEIT, 2022)

FUME: An air quality decision support system for cities based on CEP technology and fuzzy logic. - Enrique Brazález; Hermenegilda Macià; Gregorio Díaz 001; María-Teresa Baeza-Romero; Edelmira Valero; Valentín Valero (Appl. Soft Comput., 2022)

PITS: An Intelligent Transportation System in pandemic times. - Enrique Brazález; Hermenegilda Macià; Gregorio Díaz 001; Valentín Valero; Juan Boubeta-Puig (Eng. Appl. Artif. Intell., 2022)

Reducing the number of migrated instances during business process change: A graph rewriting approach. - Mohammed Mounir Bouhamed; Allaoua Chaoui; Radouane Nouara; Gregorio Díaz 001; Abderraouf Dembri (J. King Saud Univ. Comput. Inf. Sci., 2022)

A Compositional Approach for Complex Event Pattern Modeling and Transformation to Colored Petri Nets with Black Sequencing Transitions. - Valentín Valero; Gregorio Díaz 001; Juan Boubeta-Puig; Hermenegilda Macià; Enrique Brazález (IEEE Trans. Software Eng., 2022)

An Intelligent Transportation System for Tsunamis Combining CEP, CPN and Fuzzy Logic. - Gregorio Díaz 001; Hermenegilda Macià; Enrique Brazález; Juan Boubeta-Puig; M. Carmen Ruiz; Valentín Valero (ICCS (1), 2023)

Designing a Fault Detection System for Wind Turbine Control Monitoring Using CEP. - Enrique Brazález; Gregorio Díaz 001; Hermenegilda Macià; Valentín Valero (IWANN (2), 2023)

ITS4Tsunamis: An Intelligent Transportation System for tsunami emergencies. - Gregorio Díaz 001; Hermenegilda Macià; Enrique Brazález; Juan Boubeta-Puig; M. Carmen Ruiz; Valentín Valero (J. Comput. Sci., 2024)