Model Checking has become one of the most powerful methods for automatic
verification of software systems. However it is widely accepted that this
technique is only usable when the behavior of the system to be analyzed
is given by small models, in order to avoid the state explosion problem.
This page presents aSPIN, a XML-based
tool for obtaining abstract versions from models written in PROMELA, which
can be verified with the model checker SPIN. The tool follows the theoretical
basis presented in (GM99) (GMP02b) and
(11/24/03): Now available the aSPIN0.9-20031124 distribution
package for Windows. This update includes new abstraction libraries: the POINT and ZERO ones.
The new package is been tested in order to verify a complex elevator system, also available here.
If you are interested in additional information, please contact
aSPIN uses the open source framework.
This is a basic air conditioned model in Promela and the XML version
The abstracted XML version (T variable) and translated again to Promela
(A Promela DTD is provided to verify
any XMLPromela document). The examples above can be seen on-line with Microsoft
These are a few snapshots of the tool. We are currently working on it.
(In case of experiencing any download problem, please contact with Jesus Martinez).
(GM99) M.M. Gallardo and P. Merino. A Framework
for Automatic Construction of Abstract Promela Models.
Theoretical and Practical Aspects of Spin Model Checking , LNCS-1680, Springer, (1999), 184--199. pdf, ps .
(GM00) M.M. Gallardo and P. Merino. A practical
method to integrate abstractions into SDL and MSC based tools.
Proc. of the 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, pages 84--89. GMD Report 91, 2000.
(GMM01) M.M Gallardo, J. Martinez, P. Merino and
S. Rosales. Using XML to Abstract Promela Models.
Proceedings of the 2002 ACM symposium on applied computing. Madrid, 2002. pg 1021-1025
(GMP01a) M.Gallardo, P.Merino, E.Pimentel. Abstract
Satisfiability of Linear Temporal Logic.
Primeras Jornadas sobre Programación y Lenguajes, 2001.
(GMP02a) M.Gallardo, P.Merino, E.Pimentel. Debugging
UML Designs with Model Checking.
Journal of Object Technology, to appear, 2002.
(GMP02b) 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.
(GMP02c) M. M. Gallardo, P.Merino, E.Pimentel.
Refinement of LTL Formulas for Abstract Model Checking
Proc. of the 9th International Static Analysis Symposium SAS '02 (September 2002)
Lecture notes in Computer Science v. 2477.
(GMMP02a) M.M Gallardo, J. Martinez, P. Merino
and E. Pimentel. aSPIN: Extending
SPIN with Abstraction.
9th International SPIN Workshop, Grenoble, France 2002, LNCS 2318, pg 254-258
(GMMP02b) M. M. Gallardo, J. Martínez, P. Merino, E. Pimentel
A Tool for Abstraction in Model Checking
7th International Workshop on Formal Methods for Industrial Critical Systems (July 2002)
Electronic Notes in Theoretical Computer Science. Vol. 66.2
(GMMP02d) M. M. Gallardo, P.Merino, E.Pimentel. Comparing Under and
Over-Approximations of LTL Properties for Model Checking
11h International Workshop on Functional and (Constraint) Logic Programming (June 2002)
Electronic Notes in Theoretical Computer Science vol. 76
XML specifications and drafts related are found in the W3C website.
Do you work (or plan to work) with SPIN? Then visit the SPIN homepage.
We have also a web intended to help SPIN based developments. You can
navigate through the source code from various SPIN distributions here.
Jesus Martinez Cruz
Pedro Merino Gomez
And of course, our past and current students:
Maria Estefania Rosales Montes
Jorge Molina Mora
Last Modification Date: 11/24/03