Article

Modere: the model-checking engine of Rebeca

Authors:

Mohammad Mahdi Jaghoori,

Marjan SirjaniAuthors Info & Claims

SAC '06: Proceedings of the 2006 ACM symposium on Applied computing

Pages 1810 - 1815

https://doi.org/10.1145/1141277.1141704

Published: 23 April 2006 Publication History

Abstract

Rebeca is an actor-based language with formal semantics that can be used in modeling concurrent and distributed software and protocols. Automatic verification of these systems in the design stage helps develop error free systems. In this paper, we describe the model checking tool developed for verification of Rebeca models. This tool uses partial order reduction technique for reducing the size of the state space generated for a given model. Using this tool for model checking Rebeca yields much better results than the previous attempts for model checking Rebeca.

References

[1]

G. Agha. The structure and semantics of actor languages. In Proc. REX Workshop, pages 1--59, 1990.

Digital Library

[2]

D. Bosnacki. Enhancing State Space Reduction Techniques for Model Checking. PhD thesis, Technische Universiteite Eindhoven, 2001.

[3]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999.

Digital Library

[4]

E. Emerson and A. Sistla. Symmetry and model checking. Formal Methods in System Design, 9(1--2):105--131, 1996.

Digital Library

[5]

E. A. Emerson, S. Jha, and D. Peled. Combining partial order and symmetry reductions. In E. Brinksma, editor, TACAS '97, volume 1217 of LNCS, pages 19--34. Springer 1997.

Digital Library

[6]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An approach to the State-Explosion Problem, PhD thesis, 1995.

[7]

C. Hewitt. Procedural embedding of knowledge in planner. In Proc. 2nd International Joint Conference on Artificial Intelligence, pages 167--184, 1971.

Digital Library

[8]

G. J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279--295, 1997.

Digital Library

[9]

G. J. Holzmann and D. Peled. An improvement in formal verification. In D. Hogrefe and S. Leue, editors, 7th IFIP WG6.1 International Conference on Formal Description Techniques, pages 197--211, 1994.

Digital Library

[10]

G. J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In Proc. Second SPIN Workshop, pages 23--32, 1996.

[11]

T. Hune, J. Romijn, M. Stoelinga, and F. W. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming (JLAP), 52-53:183--220, 2002.

[12]

C. lp and D. Dill. Better verification through symmetry. Formal methods in system design, 9(1-2):41--75, 1996.

Digital Library

[13]

K. McMillan. Symbolic Model Checking. Kluwer Academic, Boston, MA, USA, 1993.

Digital Library

[14]

NuSMV user manual. http://nusmv.irst.itc.it/NuSMV/userman/index-v2.html.

[15]

Rebeca homepage. http://khorshid.ut.ac.ir/~rebeca/.

[16]

M. Sirjani, A. Movaghar, A. Shali, and F. S. de Boer. Modeling and verification of reactive systems using Rebeca. Fundamamenta Informaticae, 63(4):385--410, 2004.

Digital Library

[17]

M. Sirjani, A. Shali, M. M. Jaghoori, H. Iravanchi, and A. Movaghar. A front-end tool for automated abstraction and modular verification of actor-based models. In IEEE ACSD 2004, pages 145--150, 2004.

Digital Library

[18]

M. Y. Vardi and P. Wolper. An automata theoretic approach to automatic program verification. In D. Kozen, editor, LICS, pages 322--331, 1986.

Cited By

Lin SManerkar YLohstroh MPolgreen EYu SJerad CLee ESeshia S(2023)Towards Building Verifiable CPS using Lingua FrancaACM Transactions on Embedded Computing Systems10.1145/360913422:5s(1-24)Online publication date: 31-Oct-2023
https://dl.acm.org/doi/10.1145/3609134
Khamespanah ESirjani MKhosravi R(2023)Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family ModelsFundamentals of Software Engineering10.1007/978-3-031-42441-0_6(72-87)Online publication date: 30-Aug-2023
https://doi.org/10.1007/978-3-031-42441-0_6
Chong WDrieberg MJeoti VAhmad R(2021)Analytical modelling of false blocking problem in wireless ad hoc networksPeer-to-Peer Networking and Applications10.1007/s12083-021-01156-9Online publication date: 2-Oct-2021
https://doi.org/10.1007/s12083-021-01156-9
Show More Cited By

Index Terms

Modere: the model-checking engine of Rebeca
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Rebeca: theory, applications, and tools
FMCO'06: Proceedings of the 5th international conference on Formal methods for components and objects

Rebeca is an actor-based language with a formal foundation for modeling concurrent and distributed systems which is designed in an effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported by a tool-set ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '06: Proceedings of the 2006 ACM symposium on Applied computing

April 2006

1967 pages

ISBN:1595931082

DOI:10.1145/1141277

Conference Chair:
Hisham M. Haddad
Kennesaw State University, Kennesaw, Georgia

Copyright © 2006 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: 23 April 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC06

Sponsor:

SIGAPP

SAC06: The 2006 ACM Symposium on Applied Computing

April 23 - 27, 2006

Dijon, France

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

23
Total Citations
View Citations
211
Total Downloads

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

Reflects downloads up to 25 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lin SManerkar YLohstroh MPolgreen EYu SJerad CLee ESeshia S(2023)Towards Building Verifiable CPS using Lingua FrancaACM Transactions on Embedded Computing Systems10.1145/360913422:5s(1-24)Online publication date: 31-Oct-2023
https://dl.acm.org/doi/10.1145/3609134
Khamespanah ESirjani MKhosravi R(2023)Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family ModelsFundamentals of Software Engineering10.1007/978-3-031-42441-0_6(72-87)Online publication date: 30-Aug-2023
https://doi.org/10.1007/978-3-031-42441-0_6
Chong WDrieberg MJeoti VAhmad R(2021)Analytical modelling of false blocking problem in wireless ad hoc networksPeer-to-Peer Networking and Applications10.1007/s12083-021-01156-9Online publication date: 2-Oct-2021
https://doi.org/10.1007/s12083-021-01156-9
Khamespanah ESirjani MSabahi Kaviani ZKhosravi RIzadi M(2015)Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition systemScience of Computer Programming10.1016/j.scico.2014.07.00598:P2(184-204)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.005
Herber PGlesner S(2015)Verification of Embedded Real-time SystemsFormal Modeling and Verification of Cyber-Physical Systems10.1007/978-3-658-09994-7_1(1-25)Online publication date: 6-Jun-2015
https://doi.org/10.1007/978-3-658-09994-7_1
Sigurdarson SSirjani MBjörnsson YReynisson A(2013)Guided Search for Deadlocks in Actor-Based ModelsFormal Aspects of Component Software10.1007/978-3-642-35861-6_15(242-259)Online publication date: 2013
https://doi.org/10.1007/978-3-642-35861-6_15
Khamespanah ESabahi Kaviani ZKhosravi RSirjani MIzadi MAgha GBordini RMarron ARicci A(2012)Timed-rebeca schedulability and deadlock-freedom analysis using floating-time transition systemProceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions10.1145/2414639.2414645(23-34)Online publication date: 21-Oct-2012
https://dl.acm.org/doi/10.1145/2414639.2414645
Nobakht Bde Boer FJaghoori MSchlatte ROssowski SLecca P(2012)Programming and deployment of active objects with application-level schedulingProceedings of the 27th Annual ACM Symposium on Applied Computing10.1145/2245276.2232086(1883-1888)Online publication date: 26-Mar-2012
https://dl.acm.org/doi/10.1145/2245276.2232086
Sabouri HKhosravi R(2012)Reducing the Model Checking Cost of Product Lines Using Static Analysis TechniquesFormal Aspects of Component Software10.1007/978-3-642-35743-5_18(296-312)Online publication date: 2012
https://doi.org/10.1007/978-3-642-35743-5_18
Sirjani MJaghoori M(2011)Ten years of analyzing actorsFormal modeling10.5555/2074591.2074596(20-56)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2074591.2074596
Show More Cited By

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.

Figures

Tables

Media

View Table of Conten