Pedro Merino
Gómez
Associate
Professor (Profesor Titular de Universidad)
|
|
Página en
castellano
Address: Dpto. de Lenguajes y Ciencias de la Computación E.T.S.I Telecomunicación Universidad de Málaga
Campus de Teatinos. 29071
Málaga. SPAIN.
Tel: +34 (5) 213 2752 Fax: +34 (5)
213 1397 Email: pedro@lcc.uma.es
Teaching
Course 2004/2005
Software Reliability
Methods (PhD students)
Protocol Engineering
(Computer Engineering)
Communication Software (Telecommunication
Engineering)
Communication Software Lab. (Telecommunication
Engineering)
Previous
Courses
Techniques for
Automatic Analysis of Software (PhD students)
Communication Software Lab.
(Telecomunication Engineering - Bachelor)
Computer Networks (Telecomunication Engineering)
Data Communication Software (Computer Engineering)
Design and
Management of Computer Networks (Computer Engineering)
Research
Member of GISUM (Software engineering
Group at the University of Málaga)
Current
Research Interests
Specification, Verification, Analysis and
Testing of Computer Protocols and Software Systems
Abstraction and Model Checking (aSPIN is our free
tool for adding abstraction to
SPIN)
Active Networks
Past Research Lines
Implementation of Logic Programming Languages
Participation in Research Organizations
- ERCIM
(the
European Research Consortium for Informatics and Mathematics)
- SpaRCIM (the Spanish Research
Consortium for Informatics and Mathematics)
- ERCIM FMICS Working group
- CoLogNET
Network of Excelence (European Network Founded by Future and Emerging Technologies IST
Programme)
- SDL Forum
Participation in
Programme Committees
ˇ
DSVV'00(International Workshop on Distributed Systems
Validation and Verification ), Taipei , Taiwan, ROC,April 11 - 13, 2000. PC Chair: Pao-Ann Hsiung .
ˇ
FMICS'2001 (6th International Workshop on
Formal Methods for Industrial Critical Systems), Paris, France, July 16-17, 2001. PC Chairs:
Stefania Gnesi and Ulrich Ultes-Nitche.
ˇ
FMICS'2002(7th International Workshop on
Formal Methods for Industrial Critical Systems), Málaga, Spain, June 12-13, 2002. PC Chairs:
Hubert Garavel and Rance Cleaveland
ˇ
VVEIS'2003(1st International Workshop on
Verification and Validation of Enterprise Information Systems), Angers, France, April 22, 2003. PC
Chairs: Juan Carlos Augusto and Ulrich Ultes-Nitche.
ˇ
FMICS'2003(8th International Workshop on
Formal Methods for Industrial Critical Systems), Trondheim, Norway, June 5-7, 2003. PC Chairs:
Thomas Arts and Wan Fokkink.
ˇ
VVEIS'2004(2nd International Workshop on Verification
and Validation of Enterprise Information Systems), Angers, France, April 22, 2003. PC Chairs:
Juan Carlos Augusto and Ulrich Ultes-Nitche.
ˇ
SPIN 2004 (11th
International SPIN Workshop on Model Checking of Software), Barcelona,
Spain, April 1-3, 2004. PC Chair: Susanne Graf.
ˇ
TELECOM I+D 2004 (XIV Jornadas Telecom I+D), Madrid-Barcelona-Valencia-Málaga,
Spain, November 23-25, 2005. PC
Chair: Mari Satur Torre Calero.
ˇ
ISSRE04:WITUL (ISSRE04 Workshop on Integrated-reliability with Telecommunications and UML Languages), November 2, IRISA Rennes France, 2004. PC Chair: Dieter Hogrefe.
ˇ
VVEIS'2005(3rd International Workshop on Verification
and Validation of Enterprise Information Systems), Miami, USA, May 24, 2005. PC Chairs: Juan
Carlos Augusto and Ulrich Ultes-Nitche.
ˇ JITEL'2005(V Jornadas de Ingeniería Telemática), Vigo, Spain, September 12-44, 2005. PC Chair: José Juan Pazos Arias.
ˇ TELECOM I+D 2005 (XV Jornadas Telecom I+D), Madrid-Barcelona-Valencia-Málaga, Spain, November, 2005.
Organization of events
ˇ
FMICS'2002 (7th International
Workshop on Formal Methods for Industrial Critical Systems), Málaga, Spain, June 12-13, 2002. Organization Chair.
ˇ
ERCIM Meetings 2004, Málaga, Spain, June 12-13, 2002. Organization
co-Chair.
ˇ
TELECOM
I+D 2003, 2004 ( Jornadas Telecom I+D), Organization Chair in
Malaga.
Publications
M. M.
Gallardo, J. Martínez and P.Merino,
”Model Checking Active Networks with SPIN“
Computer Communications
In Press
Abstract. Recent advances in languages and
execution environments (EEs) for active networks make it now possible to
develop applications with this new exciting approach. In particular, active
networks have proven to be very suitable for multicast services. Nevertheless,
to open the network nodes to the code written by users requires the use of
analysis techniques to avoid the degradation of the network performance. Model
checking is one of the most powerful techniques to ensure software reliability.
This technique has been successfully applied to many protocols developed with
the classic (non-active) approach. Our aim is to extend its application to the
area of active protocols. The paper consists of two main contributions: (a) a
clear scheme to use the language PROMELA in order to formalize different elements in the active service (network
EE, capsules and user applications) and (b) the practical (and successful)
application of the approach to analyze an active multicast protocol using the
model checker SPIN.
M. M.
Gallardo, P.Merino, E.Pimentel
”A Generalized Semantics of Promela for Abstract Model Checking “
Formal Aspects of Computing
Volume 16, Number 3, August 2004 , Pages: 166 -
193
Abstract. Semantics of description languages
for complex systems are a central issue for implementing verification methods
such as abstract model checking. This technique is employed to verify
systems by inspecting only a small state space that represents its potential
behaviors. This paper presents a generalized operational semantics of the
modelling language Promela that provides the theoretical basis to introduce
this promising method in the model checker SPIN. The generalization consists of
identifying language aspects affected by the abstraction. Using these aspects
as parameters, it is possible to obtain and relate different interpretations of
the language. The new semantics provides a framework to reason about how to
construct the tool 
spin as an extension of spin.
María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
“aSPIN: A Tool for Abstract Model Checking”
International Journal on Software
Tools for Technology Transfer
Volume 5, Numbers 2-3
, March 2004 , Pages: 165 - 184
Abstract Abstraction methods have become one
of the most interesting topics in the automatic verification of software
systems because they can reduce the state space to be explored and allow model
checking of more complex systems. Nevertheless, there is a lack of tools
actually supporting this technique. One direction for abstracting a system is
to transform its formal description (its model) into a simpler version
specified in the same language, thus skipping the construction of a specific
(model checking) tool for the abstract model. The abstraction of the model
should be followed by the abstraction of the temporal formulas to be checked.
This paper presents spin, a tool for the integration of
abstraction (for models and formulas) into the well-known model checker spin.
We present the theoretical results supporting the implementation together with
a case study.
María del Mar Gallardo,
Jesús Martínez, Pedro Merino and Ernesto Pimentel
”Applying Data Abstraction to XML Formal Designs”
4th International Conference on Software Engineering, Artificial Intelligence,
Networking, and
Parallel/Distributed Computing (SNPD'03)
Lübeck, Germany October 16-18, 2003
María del Mar Gallardo,
Jesús Martínez, Pedro Merino and Ernesto Pimentel
”Abstract Model Checking and Refinement of Temporal Logic in aSPIN “
Third International Conference on
Application of Concurrency to System Design
18-20th of June 2003, Guimarăes, Portugal
María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel ,
“Transforming
Specifications to verify Embedded Systems”
ERCIM News No. 52, January 2003
J. López, A. Mańa,
P. Merino, J.M Troya,.
“The Role of Smartcards in Practical
Information Security”.
ERCIM News, Vol. 49, pp
38-40, ERCIM, April 2002.
G.
Rodríguez, P. Merino, M. M. Gallardo
” An extension of the ns simulator for active network research
“
Computer Communications
Volume 25, Number 3, February 2002 , Pages: 189 - 197
Abstract. Active Networks (ANs) represent a
new paradigm of computer network, which will enable new Internet applications
and services and improve end-to-end performance of the existing ones. However,
ANs being an emerging technology, there is still a significant lack of tools
for the design and evaluation of active network protocols. In particular, network
simulators have proven to be very valuable tools and they have been widely used
in the Internet research community. In this paper, we present a novel extension
for the well-known network simulator ns to incorporate AN support. Our
solution is versatile yet powerful, providing a consistent framework for
researchers to design and evaluate active protocols.
M. M.. Gallardo, P.Merino,
E.Pimentel
" Refinement of LTL Formulas for Abstract Model Checking"
In Proc. of the 9th International
Static Analysis Symposium SAS '02 (September 2002)
Lecture notes in Computer Science
v. 2477
M. M. Gallardo, P.Merino, E.Pimentel
"Comparing Under and Over-Approximations of LTL Properties for
Model Checking"
In Proc. of the 11h International Workshop on Functional and (Constraint)
Logic Programming (June 2002)
Electronic Notes in Theoretical
Computer Science vol. 76
M. M. Gallardo, J. Martínez, P. Merino, E. Pimentel
"A Tool for Abstraction in Model Checking"
In Proc. of the 7th International Workshop on Formal Methods for
Industrial Critical Systems (July 2002)
Electronic Notes in Theoretical
Computer Science. Vol. 66.2
M. M. Gallardo, J. Martínez, P. Merino, E. Pimentel
" aSPIN: Extending SPIN with Abstraction "
Proc. of the 9th International SPIN Workshop on Model Checking of
Software. Grenoble, France 2002, LNCS 2318, pg 254-258
M. M. Gallardo, J. Martínez, P. Merino, E. Rosales
"Using XML to implement Abstraction for Model Checking"
Proc. of the ACM Symposium on Applied Computing, SAC 2002. pg. 1021-1025
M. M. Gallardo, P.Merino, E.Pimentel
"Debugging UML Designs with Model Checking"
in Journal of Object Technology, vol. 1, no. 2, July-August 2002, pages
101-117
http://www.jot.fm/issues/issue_2002_07/article1
M. M. Gallardo, P.Merino, E.Pimentel,
" Verifying Abstract LTL Properties on Concurrent Systems "
Proc. of the 6th World Conference on Integrated Design & Process
Technology. (2002).
M.M.
Gallardo y P. Merino
"A Practical Framework to Integrate Abstractions into SDL and MSC
based Tools"
5th International Workshop on Formal Methods for Industrial Critical
Systems, Berlin (2000) 225-246.
M.M. Gallardo y P. Merino
"A Framework for Automatic Construction of Abstract Promela Models"
Theoretical and Practical Aspects of SPIN Model Checking, D. Dams, R. Gerth, S.
Leue y M. Massink. (Eds.), Springer, 1999, pp: 184-199
One of the current trends
in model checking for the verification of concurrent systems is to reduce the
state space produced by the model, and one of the more promising ways to
achieve this objective is to support some kind of automatic construction of
more abstract models. This paper presents a proposal in this direction. The
main contribution of the paper is the definition of a semantics framework which
allows us to relate different models of the system, each one with a particular
abstraction level. Automatic source-to-source transformation is supported by
this formal basis. The method is applied to Promela models.
P. Merino
"Linear Observers: A property Language for Protocol Verification
"
Ph D. Thesis, University of Malaga, (only Spanish).(Summary at LOPSTR98)
P. Merino y J.M. Troya
"Modelling and Verification of the MCS Layer with SPIN"
DIMACS Series in Discrete Methematics and Computer Science, Vol. 32, American
Mathematical Society, 1997, pp:101-111. (Improved version of 5th SPIN paper)
P. Merino y J.M. Troya
"Verifying Protocols with Executable Linear Logic"
Logic-Based Program Synthesis and Transformation (LOPSTR) , Reino Unido, 1998,
pp:88-95
This paper describes a new
formalism for the specification and automatic verification of temporal
properties where the counting and the distinction of the events are critical in
deciding the correctness of systems. The specification formalism is based on
giving an operational interpretation to a fragment of Linear Logic, which is
specially suitable to express counting and changes between states. This
operational semantics gives us a natural way to implement a model- checking
algorithm in a similar way to the automata-theoretic approach to verification
M.M. Gallardo, P. Merino y J.M. Troya
"Relating Abstract Interpretation with Logic Program Verification"
Verification, Model Checking and Abstract Interpretation, EEUU, 1997, pp:
The aim of this work is to
show the natural connection that exists between logic program verification and
abstract interpretation. Briefly, the latter technique consists of proving
whether a certain property is verified by a given program. This property is a
representation (an abstraction) of the set of standard states which verify it.
This is why abstract interpretation is considered as an abstract execution of
programs, using descriptions instead of standard data.
P. Merino y J.M. Troya
"EVP: Integration of FDTs for the analysis and verification of
communication protocols"
Computer Aided Verification, R. Alur . y T.A. Henzinger. (Eds.), Springer,
1996, pp:406-410
EVP is an integrated
toolset for specification and analysis of communication protocols and
distributed systems. Specifications in standard Formal Description Techniques
(FDTs) like SDL or LOTOS are translated into a common language, and then
analyzed with tools for this internal representation. The common language is a
concurrent logic language specially designed for distributed programming. The
analysis consists in interactive simulation and automatic verification. The
topic of this paper is the current status and applications of the EVP
environment.
P. Merino y J.M. Troya
"A Logic Based Approach to Validation and Verification of Computer
Protocolos"
ERCIM Workshop on Formal Methods for Industrial Critical Applications , Reino
Unido, 1996, pp: 109-124
This paper presents a
language to combine the use of logic based formalisms for modeling concurrent
systems with recent optimisation techniques for state-space based verification.
Our approach is the integration of suitable logics into the declarative
language CLT to specify both the protocol design and its desired requirements.
We define a transition semantics for the language that, preserving the
advantages of its logic basis, allows efficient methods to perform the
validation of general properties and the verification of particular
requirements. CLT is a concurrent language based on Horn-clause logic, Girard’s
linear logic and linear time temporal logic. A variant of the concurrent logic
languages, which are based on Horn-clause logic, is the part to specify the
protocol design. Linear logic is employed to express temporal properties in the
context of the automata-theoretic approach to model-checking. We find out taht
this logic can be a powerful formalism to fill the gap between temporal
logic and automata for some class temporal properties. Finally, a restricted
temporal logic is employed to express the most simple properties without
defining automata. The language is being demonstrated as a suitable formalism
to specify concurrent systems, and is being used specially for computer
protocols. In this paper, the syntax and formal semantics of CLT and a helpful
example are given; also some proposals about its tool support are
presented.
P. Merino y J.M. Troya
"Modelling and Verification of the MCS Layer with SPIN"
The 2nd International Workshop on the SPIN Verification, EEUU, 1996, pp: 60-71
This paper presents the
first results of work in progress aimed at using the SPIN tool for the verification
of multi-party protocols. We focus on the ITU-T Multipoint Communication
Service, a generic service designed to support highly-interactive multimedia
conferencing. We have built a formal Promela model of the protocol recommended
for this layer, and have described some requirements using linear-time temporal
logic. Next, we have verified this model against these properties using the
model-checking capabilities of the SPIN tool. This analysis
demonstrates that most of the properties are satisfied, but also that the
interpretation of the standard documents could introduce some errors in a real
implementation. Apart from the verification of the protocol itself, the
aim of the work is the evaluation of Promela and SPIN for multi-party protocols
such as the ones employed for multiconferencing or collaborative environments.
In this case, we detect some deficiencies in Promela for modelling certain
aspects of the protocol behaviour and also for formalising various temporal
requirements. We have suggested some extensions to improve the language
Return to Dpt.
|
|
Please, send me your comments |
