Article

Formal modelling and verification of a component model using coloured petri nets and model checking

Authors:

Elthon Oliveira,

Hyggo Almeida,

Leandro SilvaAuthors Info & Claims

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

Pages 1427 - 1431

https://doi.org/10.1145/1244002.1244309

Published: 11 March 2007 Publication History

Get Access

Abstract

Component based software engineering has been claimed as a suitable approach to improve the flexibility and reuse in software development. In this context, the Compor infrastructure provides mechanisms to promote the dynamic composition of software systems, addressing applications with support for unanticipated requirement changes. In this paper, the formal modelling and verification of the COMPOR component model is presented. Hierarchical Colored Petri Nets are used for modelling and simulation, purposing to show the correct behavior for some scenarios. Model checking is used to prove that the scenarios analyzed with simulation are correct for all possible behaviors of the model.

References

[1]

H. O. Almeida, A. Perkusich, G. V. V. de Melo Ferreira, E. C. L. Filho, and E. de Barros Costa. A Component Model to Support Dynamic Unanticipated Software Evolution. In SEKE '06: Proceedings of International Conference on Software Engineering and Knowledge Engineering, pages 262--267, San Francisco, USA, 2006.

Google Scholar

[2]

H. O. Almeida, L. D. Silva, E. S. Oliveira, and A. Perkusich. A Formal Approach for Component Based Embedded Software Modelling and Analysis. In Proceedings of IEEE International Symposium on Industrial Electronics - ISIE'05, to appear, Croatia, 2005.

Google Scholar

[3]

S. Christensen and K. H. Mortensen. Design/CPN ASK-CTL Manual. University of Aarhus, 1996.

Google Scholar

[4]

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

Digital Library

Google Scholar

[5]

I. Crnkovic. Component-based Software Engineering - New Challenges in Software Development. In Software Focus, volume 4, pages 127--133. Willey, Dezembro 2001.

Google Scholar

[6]

K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis, Methods and Practical Use. EACTS - Monographs on Theoretical Computer Science. Springer-Verlag, 1992.

Digital Library

Google Scholar

[7]

K. Jensen and et al. Design/CPN 4.0. Meta Software Corporation and Department of Computer Science, University of Aarhus, Denmark, 1999. On-line version:http://www.daimi.au.dk/designCPN/.

Google Scholar

[8]

C. Szypersky. Component Software, Beyond Object-Oriented Programming. Addison-Wesley, 1998.

Digital Library

Google Scholar

Cited By

View all

Garfatta IKlai KGraïet MGaaloul WHong JBures MPark JCerny T(2022)Model checking of vulnerabilities in smart contractsProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507309(316-325)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507309
Yang RDing ZGuo TPan MJiang C(2022)Model Checking of Variable Petri Nets by Using the Kripke StructureIEEE Transactions on Systems, Man, and Cybernetics: Systems10.1109/TSMC.2022.316374152:12(7774-7786)Online publication date: Dec-2022
https://doi.org/10.1109/TSMC.2022.3163741
Ye QMacgregor M(2011)Using simulation to test formally verified protocols in complex environmentsMathematical and Computer Modelling: An International Journal10.1016/j.mcm.2010.03.03953:3-4(538-551)Online publication date: 1-Feb-2011
https://dl.acm.org/doi/10.1016/j.mcm.2010.03.039
Show More Cited By

Index Terms

Recommendations

TCTL Model Checking of Time Petri Nets

We consider Time Petri Nets (TPN) for which a firing time interval is associated with each transition. State space abstractions for TPN preserving various classes of properties (LTL, CTL and CTL^*) can be computed, in terms of so called state classes. ...
From Petri Nets to colored Petri Nets: a tutorial introduction to nets based formalism for modeling and simulation
WSC '19: Proceedings of the Winter Simulation Conference

Petri Net, a widely studied mathematical formalism, is a graphical notation for modeling systems. Petri Nets provide the foundation for modeling concurrency, communication, synchronization, and resource sharing constraints that are inherent to many ...
Model checking object petri nets in prolog
PPDP '04: Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming

Object Petri nets (OPNs) provide a natural and modular method for modelling many real-world systems. We give a structure-pre-serving translation of OPNs to Prolog by encoding the OPN semantics, avoiding the need for an unfolding to a flat Petri net. The ...

Comments

Information & Contributors

Information

Published In

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

March 2007

1688 pages

ISBN:1595934804

DOI:10.1145/1244002

Conference Chairs:
Yookun Cho
Seoul National University, Seoul, Korea
,
Roger L. Wainwright
University of Tulsa, Tulsa, Oklahoma
,
Hisham M. Haddad
Kennesaw State University, Kennesaw, Georgia
,
Sung Y. Shin
South Dakota State University, Brookings, South Dakota
,
Program Chair:
Yong Wan Koo
The University of Suwon, Gyeongggi-do, Korea

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 March 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SAC07

Sponsor:

SIGAPP

SAC07: The 2007 ACM Symposium on Applied Computing

March 11 - 15, 2007

Seoul, Korea

Acceptance Rates

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

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
322
Total Downloads

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

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Garfatta IKlai KGraïet MGaaloul WHong JBures MPark JCerny T(2022)Model checking of vulnerabilities in smart contractsProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507309(316-325)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507309
Yang RDing ZGuo TPan MJiang C(2022)Model Checking of Variable Petri Nets by Using the Kripke StructureIEEE Transactions on Systems, Man, and Cybernetics: Systems10.1109/TSMC.2022.316374152:12(7774-7786)Online publication date: Dec-2022
https://doi.org/10.1109/TSMC.2022.3163741
Ye QMacgregor M(2011)Using simulation to test formally verified protocols in complex environmentsMathematical and Computer Modelling: An International Journal10.1016/j.mcm.2010.03.03953:3-4(538-551)Online publication date: 1-Feb-2011
https://dl.acm.org/doi/10.1016/j.mcm.2010.03.039
Guoyin ZMing LAihong Y(2010)A Coloured Petri Net Based Formal Verification Methodology of MVB-TCN DeviceProceedings of the 2010 International Conference on Intelligent Computation Technology and Automation - Volume 0110.1109/ICICTA.2010.72(46-49)Online publication date: 11-May-2010
https://dl.acm.org/doi/10.1109/ICICTA.2010.72
Guoyin Zhang Ming Liu Aihong Yao (2010)A formal approach for modeling and verification of bus bridge based on Petri Net and model checking2010 3rd International Conference on Computer Science and Information Technology10.1109/ICCSIT.2010.5565021(335-339)Online publication date: Jul-2010
https://doi.org/10.1109/ICCSIT.2010.5565021

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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

TCTL Model Checking of Time Petri Nets

From Petri Nets to colored Petri Nets: a tutorial introduction to nets based formalism for modeling and simulation

Model checking object petri nets in prolog

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations