Article

Using XML to implement abstraction for Model Checking

Authors:

María del Mar Gallardo,

Jesús Martínez,

Estefanía RosalesAuthors Info & Claims

SAC '02: Proceedings of the 2002 ACM symposium on Applied computing

Pages 1021 - 1025

https://doi.org/10.1145/508791.508989

Published: 11 March 2002 Publication History

Abstract

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. The paper presents αSPIN, an XML-based tool for obtaining abstract versions from a given model written in PROMELA, which can be verified with the model checker SPIN. This tool follows the theoretical basis presented in [9].

References

[1]

P. B. S. Abiteboul, D. Suciu. Data on the Web : >From Relations to Semistructured Data and Xml. Morgan Kaufmann Publishers, 1999.]]

Digital Library

[2]

E. Clarke, E. A. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244-263, 1986.]]

Digital Library

[3]

E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Trans. on Programming Languages and Systems, 16(5):1512-1245, 1994.]]

Digital Library

[4]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 2000.]]

Digital Library

[5]

J. C. Cleaveland. Program Generators with XML and Java. Prentice-Hall, 2001.]]

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symp. on Principles of Programming Languages, pages 238-252, 1977.]]

Digital Library

[7]

D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM TOPLAS, 19(2):253-291, 1997.]]

Digital Library

[8]

D. Dams, R. Gert, S. Leue, and M. Massink, editors. Theoretical and Practical Aspects of SPIN Model Checking, volume 1680 of LNCS. Springer, 1999.]]

Digital Library

[9]

M. Gallardo and P. Merino. A framework for automatic construction of abstract promela models. In {8}, pages 184-199, 1999.]]

Digital Library

[10]

M. Gallardo and P. Merino. A practical method to integrate abstractions into SDL and MSC based tools. In Proc. of the 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, pages 84-89. GMD Report 91, 2000.]]

[11]

E. Gamma, H. Helm, R. Johnson, and J. Vlissides. Design Patterns. Addison-Wesley Pub Co., 1995.]]

[12]

G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.]]

Digital Library

[13]

G. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.]]

Digital Library

[14]

J. Hunter and B. McLaughlin. The JDOM project. Available in http://www.jdom.org, 2000.]]

[15]

C. Loiseaux, S. Graf, J. Sifakis, and S. B. A. Boujjani. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1-35, 1995.]]

Digital Library

[16]

M. W. M. Jngel, E. Kindler. Towards a generic interchange format for petri nets. In Proc. of Meeting on XML/SGML based Interchange Formats for Petri Nets, 2000.]]

[17]

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer-Verlag, New York, 1992.]]

Digital Library

[18]

αSPlN project. University of Málaga. http://www.lcc.uma.es/ gisum/fmse/tools.]]

[19]

W3Consortium. Extensible markup language (xml) 1.0 (second edition). Available in http://www.w3.org/XML/, 2000.]]

Cited By

Del Mar Gallardo MMartínez JMerino PPimentel E(2018)źSPINInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3049063.30490985:2-3(165-184)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.5555/3049063.3049098
Ma SKong ZJiang XLiang C(2010)Framework designing of boa for the development of enterprise management information systemProceedings of the 2010 international conference on Life system modeling and and intelligent computing, and 2010 international conference on Intelligent computing for sustainable energy and environment: Part I10.5555/1888466.1888490(185-195)Online publication date: 17-Sep-2010
https://dl.acm.org/doi/10.5555/1888466.1888490
Ma SKong ZJiang XLiang C(2010)Framework Designing of BOA for the Development of Enterprise Management Information SystemProceedings, Part I, of the International Conference on Life System Modeling and Intelligent Computing - Volume 632810.1007/978-3-642-15621-2_22(185-195)Online publication date: 17-Sep-2010
https://dl.acm.org/doi/10.1007/978-3-642-15621-2_22
Show More Cited By

Index Terms

Using XML to implement abstraction for Model Checking

Recommendations

Model checking XML manipulating software
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, ...
Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel ...
Model checking XML manipulating software

The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '02: Proceedings of the 2002 ACM symposium on Applied computing

March 2002

1200 pages

ISBN:1581134452

DOI:10.1145/508791

Conference Chair:
Gary B. Lamont
Air Force Institute of Technology, USA
,
Program Chairs:
Hisham Haddad
Kennesaw State Univ., USA
,
George Papadopoulos
Univ. of Cyprus, Cyprus
,
Publications Chair:
Brajendra Panda
University of Arkansas, USA

Copyright © 2002 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 March 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC02

Sponsor:

SIGAPP

SAC02: 2002 ACM Symposium on Applied Computing

March 11 - 14, 2002

Madrid, Spain

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
483
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Del Mar Gallardo MMartínez JMerino PPimentel E(2018)źSPINInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3049063.30490985:2-3(165-184)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.5555/3049063.3049098
Ma SKong ZJiang XLiang C(2010)Framework designing of boa for the development of enterprise management information systemProceedings of the 2010 international conference on Life system modeling and and intelligent computing, and 2010 international conference on Intelligent computing for sustainable energy and environment: Part I10.5555/1888466.1888490(185-195)Online publication date: 17-Sep-2010
https://dl.acm.org/doi/10.5555/1888466.1888490
Ma SKong ZJiang XLiang C(2010)Framework Designing of BOA for the Development of Enterprise Management Information SystemProceedings, Part I, of the International Conference on Life System Modeling and Intelligent Computing - Volume 632810.1007/978-3-642-15621-2_22(185-195)Online publication date: 17-Sep-2010
https://dl.acm.org/doi/10.1007/978-3-642-15621-2_22
del Mar Gallardo MMartínez JMerino PRodríguez G(2005)Integration of Reliability and Performance Analyses for Active Network ServicesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2004.08.066133(217-236)Online publication date: 1-May-2005
https://dl.acm.org/doi/10.1016/j.entcs.2004.08.066
del Mar Gallardo MMartínez JMerino PPimentel E(2004)αSPIN: A tool for abstract model checkingInternational Journal on Software Tools for Technology Transfer10.1007/s10009-003-0122-95:2-3(165-184)Online publication date: 1-Mar-2004
https://doi.org/10.1007/s10009-003-0122-9
Gallardo MMerino PPimentel E(2002)Comparing Under and Over-Approximations of LTL Properties for Model CheckingElectronic Notes in Theoretical Computer Science10.1016/S1571-0661(04)80790-476(131-144)Online publication date: Nov-2002
https://doi.org/10.1016/S1571-0661(04)80790-4
Gallardo MMartínez JMerino PPimentel E(2002)A Tool for Abstraction in Model CheckingElectronic Notes in Theoretical Computer Science10.1016/S1571-0661(04)80401-866:2(17-32)Online publication date: Dec-2002
https://doi.org/10.1016/S1571-0661(04)80401-8
del Mar Gallardo MMartínez JMerino PPimentel E(2002)αSPIN: Extending SPIN with AbstractionModel Checking Software10.1007/3-540-46017-9_24(254-257)Online publication date: 23-May-2002
https://doi.org/10.1007/3-540-46017-9_24

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents