Article

Petri nets state space analysis in the cloud

Author:

Matteo CamilliAuthors Info & Claims

ICSE '12: Proceedings of the 34th International Conference on Software Engineering

Pages 1638 - 1640

Published: 02 June 2012 Publication History

Abstract

Several techniques for addressing the state space explosion problem in model checking have been studied. One of these is to use distributed memory and computation for storing and exploring the state space of the model of a system. In this report, we present and compare different multi- thread, distributed, and cloud approaches to face the state-space explosion problem. The experiments report shows the convenience (in particular) of cloud approaches.

References

[1]

Amazon Web Services LLC. Amazon Elastic MapReduce documentation. http://aws.amazon.com/documentation/ elasticmapreduce/, 2012. Last visited: January 2012.

[2]

A. P. Atlee and H. Gannon. Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng., 19:41-55, January 1993.

Digital Library

[3]

Carlo Bellettini, Matteo Camilli, Lorenzo Capra, and Mattia Monga. State space exploration of rt systems in the cloud. CoRR, arXiv:1203.6806v1, 2012.

[4]

Carlo Bellettini and Lorenzo Capra. Reachability analysis of time basic petri nets: A time coverage approach. In SYNASC, pages 110-117, 2011.

Digital Library

[5]

Carlo Bellettini, Miguel Felder, and Mauro Pezzè. A tool for analysing high-level timed Petri nets. IPTES Esprit Project 5570 PDM-41, Politecnico di Milano, September 1993.

[6]

Bernard Berthomieu and Michel Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng., 17:259-273, March 1991.

Digital Library

[7]

Jeffrey Dean and Sanjay Ghemawat. MapReduce: simplified data processing on large clusters. Commun. ACM, 51:107- 113, January 2008.

Digital Library

[8]

Jaliya Ekanayake, Hui Li, Bingjing Zhang, Thilina Gunarathne, Seung-Hee Bae, Judy Qiu, and Geoffrey Fox. Twister: a runtime for iterative MapReduce. In Proc. of Symposium on High Performance Distributed Computing, pages 810-818, 2010.

Digital Library

[9]

Eric Freeman, Ken Arnold, and Susanne Hupfer. JavaSpaces Principles, Patterns, and Practice. Addison-Wesley Longman Ltd., Essex, UK, UK, 1st edition, 1999.

Digital Library

[10]

Hubert Garavel, Radu Mateescu, and Irina Smarandache. Parallel state space construction for model-checking. In Proceedings of the 8th international SPIN workshop on Model checking of software, SPIN '01, pages 217-234, New York, NY, USA, 2001. Springer-Verlag New York, Inc.

Digital Library

[11]

Carlo Ghezzi, Dino Mandrioli, Sandro Morasca, and Mauro Pezzè. A unified high-level Petri net formalism for timecritical systems. IEEE Trans. Softw. Eng., 17:160-172, February 1991.

Digital Library

[12]

Lars Kristensen and Laure Petrucci. An approach to distributed state space exploration for coloured petri nets. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, volume 3099 of LNCS, pages 474-483. Springer Berlin / Heidelberg, 2004.

[13]

C. Lakos and L. Petrucci. Modular state space exploration for timed Petri nets. Int. J. Softw. Tools Technol. Transf., 9:393-411, May 2007.

Digital Library

[14]

The Apache Software Foundation. Hadoop MapReduce documentation. http://hadoop.apache.org/mapreduce/, 2007. Last visited: January 2012.

[15]

Antti Valmari. The state explosion problem. In Lectures on Petri Nets I, pages 429-528, London, UK, 1998. Springer-Verlag.

Digital Library

Cited By

Bellettini CCamilli MCapra LMonga M(2016)Distributed CTL model checking using MapReduceConcurrency and Computation: Practice & Experience10.1002/cpe.365228:11(3025-3041)Online publication date: 10-Aug-2016
https://dl.acm.org/doi/10.1002/cpe.3652
Camilli MJalote PBriand LHoek A(2014)Formal verification problems in a big data world: towards a mighty synergyCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591088(638-641)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591088

Recommendations

State space analysis of Petri nets with relation-algebraic methods

A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net's state space. Since state space explosion is still a serious problem, efficiently ...
Reachability Analysis of P-time Petri Nets with Parametric Markings
ACSD '12: Proceedings of the 2012 12th International Conference on Application of Concurrency to System Design

This paper deals with the verification of P-Time Petri nets with parametric markings. It investigates the verification of reach ability properties in the case of an upward-closed set of initial markings. We propose an efficient state space abstraction ...
Non Equivalence between Time Petri Nets and Time Stream Petri Nets
PNPM '99: Proceedings of the The 8th International Workshop on Petri Nets and Performance Models

It had been shown that Merlin's Time Petri Nets are a special case of Time Stream Petri Nets. In this paper, we show that it does not exist a time equivalence between both models. We extend first this result to the nonequivalence of Timed Automata and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '12: Proceedings of the 34th International Conference on Software Engineering

June 2012

1657 pages

ISBN:9781467310673

General Chair:
Martin Glinz,
Program Chairs:
Gail Murphy,
Mauro Pezzè

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

IEEE Press

Publication History

Published: 02 June 2012

Check for updates

Qualifiers

Article

Conference

ICSE '12

Sponsor:

SIGSOFT

ICSE '12: 34th International Conference on Software Engineering

June 2 - 9, 2012

Zurich, Switzerland

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
134
Total Downloads

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

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bellettini CCamilli MCapra LMonga M(2016)Distributed CTL model checking using MapReduceConcurrency and Computation: Practice & Experience10.1002/cpe.365228:11(3025-3041)Online publication date: 10-Aug-2016
https://dl.acm.org/doi/10.1002/cpe.3652
Camilli MJalote PBriand LHoek A(2014)Formal verification problems in a big data world: towards a mighty synergyCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591088(638-641)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591088

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