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 (GMP02c)
 
 

Downloads

(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 with us.
 

aSPIN uses the  open source framework.

XML examples:

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 Explorer5.
 

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).

Publications
 

(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

Related Material
 

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.
 

People

Maria del Mar Gallardo
Jesus Martinez Cruz
Pedro Merino Gomez
Ernesto Pimentel

And of course, our past and current students:

Maria Estefania Rosales Montes
Jorge Molina Mora

           Last Modification Date:  11/24/03