Copyright Notice: The material below
is presented to ensure timely dissemination of research results.
Copyright and all rights therein are retained by authors or by other
copyright holders. All persons copying this information are expected
to adhere to the terms and constraints invoked by each author's copyright.
In all cases, the articles below may not be reposted without explicit
permission of the copyright holder.
Ph. D. Thesis
Publications (in reverse chronologically order).
- Formal Verification Of The Secure Sockets Layer
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Juan José Pardo
In Proceedings of the 10th International Conference on Enterprise Information Systems (ICEIS'08)
Barcelona (Spain), June 2008.
- Security in Wireless Sensor Networks: A Formal Approach
Llanos Tobarra, Diego Cazorla and Fernando Cuartero
Chapter 8 of the book From Problem to Solution: Wireless Sensor Networks Security
To appear in third quarter 2008.
Nova Publishers.
- Automated Verification Of Web Services Trust Issuance Binding
Llanos Tobarra, Diego Cazorla and Fernando Cuartero
In
Proceedings of the IADIS International Conference on Applied Computing (IADIS-AC'08)
Algarve (Portugal), April 2008.
IADIS Press.
- Analysis of security protocol MiniSec for Wireless Sensor Networks
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Gregorio Díaz
Presented at IV Congreso Iberoamericano de Seguridad Informática (CIBSI'07)
Mar del Plata (Argentina), November 2007
[.pdf]
[BibTeX]
- Formal Analysis of Sensor Network Encryption Protocol (SNEP)
Llanos Tobarra, Diego Cazorla and Fernando Cuartero
In Proceedings of the 3rd IEEE International Workshop on Wireless and Sensor Networks Security (WSNS 2007).
Pisa (Italy), October 2007.
IEEE Computer Society.
[.pdf]
[BibTeX]
- Model Checking Wireless Sensor Network Security Protocols: TinySec + LEAP
Llanos Tobarra, Diego Cazorla, Fernando Cuartero, Gregorio Diaz and Emilia Cambronero
In Proceedings of the First IFIP International Conference on Wireless Sensor and Actor Networks (WSAN'07).
Albacete (Spain), September 2007.
IFIP Main Series, Springer.
[.pdf]
[BibTeX]
- A Bounded True Concurrent Process Algebra and Flexible Manufacturing Systems
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero, Hermenegilda Macia
Presented at XV Jornadas de Concurrencia y Sistemas Distribuidos (JCSD'07)
Torremolinos, Málaga (Spain), June 2007
- Analysis of Web Services Secure Conversation with Formal Methods
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Gregorio Diaz
In Proceedings of the Second International Conference on Internet and Web Applications and Services (ICIW 2007).
Mauritius, May 2007.
IEEE Computer Society.
[.pdf]
[BibTeX]
- Specification and performance evaluation of Flexible Manufacturing Systems using a Bounded True Concurrent Process Algebra
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero and J. Jose Pardo
In Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation (CIMCA'06).
Sydney (Australia), November 2006.
IEEE Computer Society.
[.ps.gz]
[BibTeX]
- Process Algebra Specification of Flexible Manufacturing Systems
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero and J. Jose Pardo
In Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06).
Timisoara (Romania), September 2006.
IEEE Computer Society.
[.ps.gz]
[BibTeX]
- Computación de Altas Prestaciones en el grupo de Sistemas Concurrentes y de Tiempo Real.
Enrique Arias, Diego Cazorla, Vanesa Guijarro, Jesús Cruz
Presented at XIV Jornadas de Concurrencia y Sistemas Distribuidos (JCSD'06)
San Sebastián (Spain), June 2006
- A Bounded True Concurrency Process Algebra for Automated Verification
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero, J. José Pardo
Electronic Notes in Theoretical Computer Science, vol. ?
Presented at Fifth International Workshop on Automated Verification of Infinite-State Systems (AVIS'06)
April 2006
Elsevier Science
[.ps.gz]
[BibTeX]
- Analysis of the SET E-Commerce Protocol Using a True Concurrency Process Algebra
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero and J. José Pardo
In Proceedings of the 21st Annual
ACM Symposium on Applied Computing (SAC'06). Track on E-Commerce Technologies
Dijon (France), April 2006.
ACM Press.
[.ps.gz]
[BibTeX]
- Formal Verification of TLS Handshake and Extensions for Wireless Networks
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Gregorio Diaz
Proceedings of the
IADIS International Conference on Applied Computing (IADIS-AC'06)
San Sebastián (Spain), February 2006.
IADIS Press.
[.ps.gz]
[BibTeX]
- A Formal Specification and Performance Evaluation of the Purchase Phase in the SET Protocol
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero and J. José Pardo
In Proceedings of the 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05). Workshop on Computer-Aided Verification of Information Systems (CAVIS'05)
Timisoara (Romania), September 2005.
IEEE Computer Society.
[.ps.gz]
[BibTeX]
- Analysis of an application of Web Services Security with Formal Methods
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Gregorio Diaz
Presented at XIII Jornadas de Concurrencia y Sistemas Distribuidos (JCSD'05)
Granada (Spain), September 2005
- Application of Formal Methods to the Analysis of Web Services Security
Llanos Tobarra, Diego Cazorla, Fernando Cuartero and Gregorio Diaz
Lecture Notes in Computer Science, vol. 3670.
Presented at
2nd International Workshop on Web Services and Formal Methods (WS-FM'05)
Versailles (France), September 2005.
Springer.
[.ps.gz]
[BibTeX]
- A Bounded True Concurrency Process Algebra for Performance Evaluation
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero, J. José Pardo and Hermenegilda Macià
Lecture Notes in Computer Science, vol. 3236.
Presented at
1st European Performance Engineering Workshop (EPEW'04)
Toledo (Spain), October 2004.
Springer.
[.ps.gz]
[BibTeX]
- Introducing the Iteration in sPBC
Hermenegilda Macià, Valentín Valero, Diego Cazorla and Fernando Cuartero
Lecture Notes in Computer Science, vol. 3235.
Presented at
24th IFIP WG 6.1 Int. Conf. on Formal Techniques for Networked and Distributed
Systems (FORTE'04)
Madrid (Spain), September 2004
Springer.
[.ps.gz]
[BibTeX]
- A Realistic Model for True Concurrency
M. Carmen Ruiz, Diego Cazorla, Fernando Cuartero and J. José Pardo
Presented at XII Jornadas de Concurrencia (JJCC'04).
Las Navas del Marqués, Ávila (Spain), June 2004
- Verifiyng and Capturing Probabilistic Behaviours of Real-Time Systems
Gregorio Díaz, Diego Cazorla, Fernando L. Pelayo, Fernando Cuartero and Valentín Valero
Presented at 19th Annual UK
Performance Engineering Workshop (UKPEW'03)
Coventry (UK), July 2003
University of Warwick.
[.ps.gz]
[BibTeX]
- P_UPPAAL: A Tool for Capturing the Probabilistic Behaviour of UPPAAL Models
Gregorio Díaz, Diego Cazorla, Fernando Cuartero, Valentín Valero
Presented at XI Jornadas de Concurrencia (JJCC'03).
Benicasim (Spain), June 2003
- Analysis of the MPEG-2 Encoding Algorithm with Rosa
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
Electronic Notes in Theoretical Computer Science, vol. 80.
Presented at 8th International
Workshop on Formal Methods for Industrial Critical Systems (FMICS'03)
August 2003
Elsevier Science
[.ps.gz]
[BibTeX]
- Algebraic Theory of Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero, Fernando L. Pelayo, J. José Pardo
The Journal of Logic and Algebraic Programming, vol. 55 (1-2).
March-April 2003
Elsevier Science
[.ps.gz]
[BibTeX]
- On the Improvements of the MPEG-2 Encoding Algorithm by Timed-Arc Petri Nets
Valentín Valero, Fernando L. Pelayo, Fernando Cuartero, Diego Cazorla
In Proceedings of the 18th Annual UK
Performance Engineering Workshop (UKPEW'02).
Glasgow (Scotland), July 2002
University of Glasgow.
[.ps.gz]
[BibTeX]
- Specification and Analysis of the MPEG-2 Encoder with Timed-Arc Petri Nets
Valentín Valero, Fernando L. Pelayo, Fernando Cuartero, Diego Cazorla
Electronic Notes in Theoretical Computer Science, vol. 66(2).
Presented at 7th International
Workshop on Formal Methods for Industrial Critical Systems (FMICS'02)
December 2002
Elsevier Science
[.ps.gz]
[BibTeX]
- Analysis of the MPEG-2 Encoder Algorithm with Timed-Arc Petri Nets
Valentín Valero, Fernando L. Pelayo, Fernando Cuartero, Diego Cazorla
In Actas de las X Jornadas de Concurrencia (JJCC'02).
Jaca (Spain), June 2002
Editorial Kronos
- Automatic Translation of a Timed Process Algebra into Dynamic State Graphs
J. José Pardo, Valentín Valero, Fernando Cuartero, Diego Cazorla
In Proceedings of the
8th Asia-Pacific Software Engineering Conference (APSEC'01).
Macau (China), December 2001
IEEE Computer Society
[.ps.gz]
[BibTeX]
- Actas de las I Jornadas sobre Programación y Lenguajes
Fernando Orejas, Fernando Cuartero, Diego Cazorla (editors)
November 2001
Department of Computer Science, University of Castilla-La Mancha
- Reasoning about Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero, Fernando L. Pelayo
In Actas de las I Jornadas sobre Programación y Lenguajes (PROLE'01).
Almagro (Spain), November 2001
- A Process Algebra for Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero,Fernando L. Pelayo
Information Processing Letters, vol. 80(1).
October 2001
Elsevier Science
[.ps.gz]
[BibTeX]
- Specification and Performance of the MPEG2 Video Encoder by using the Stochastic Process Algebra:
ROSA
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
In Proceedings of the
17th Annual UK Performance Engineering Workshop (UKPEW'01).
Leeds (UK), July 2001
University of Leeds
- An Example of Performance Evaluation by Using the Stochastic Process Algebra: ROSA
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
In Proceedings
of the 7th International Conference on Real-Time Computing Systems and Applications
(RTCSA'00).
Cheju Island (South Korea), December 2000
IEEE Computer Society
[.ps.gz]
[BibTeX]
- Un Ejemplo de Evaluación Formal de Prestaciones Mediante el Álgebra de
Procesos Estocásticos: ROSA
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
In Actas de la XXVI Conferencia Latinoamericana de Informática (CLEI'00).
Monterrey (Mexico), September 2000
TEC de Monterrey
- Actas de las VIII Jornadas de Concurrencia
Diego Cazorla (editor)
June 2000
Ediciones de la UCLM
- A Denotational Model for Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero, Fernando Pelayo
In Proceedings of the 1st IEEE ICDCS
Workshop on Distributed Systems Validation and Verification (DSVV'00).
Taipei (Taiwan, ROC) April 2000
Ten H. Lai Editor
[.ps.gz]
[BibTeX]
- PPNAL: Performance Evaluation in an Algebraic Model for Probabilistic and Nondeterministic Processes
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
In Proceedings of 15th Annual UK Performance
Engineering Workshop (UKPEW'99).
Bristol (UK), July 1999
University of Bristol
- PPNAL: Evaluación de Prestaciones en un Modelo Algebraico para Procesos Probabilísticos
y No Deterministas
Fernando L. Pelayo, Fernando Cuartero, Valentín Valero, Diego Cazorla
In Actas de las VII Jornadas de Concurrencia (JJCC'99).
Gandía (Spain) June,1999
- PNAL: An Algebraic Model for Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero, J. José Pardo
In Abstracts of the 10th Nordic Workshop on Programming
Theory (NWPT'98).
Turku (Finland), October 1998
- Un Modelo Algebraico para Procesos Probabilísticos y No Deterministas
Diego Cazorla, Fernando Cuartero, Valentín Valero, J. José Pardo
In Actas de las VI Jornadas de Concurrencia (JJCC'98).
Pamplona (Spain), June 1998