research-article

Analysing timed Rebeca using McErlang

Authors:

Haukur Kristinsson,

Ehsan Khamespanah,

Brynjar Magnusson,

Marjan SirjaniAuthors Info & Claims

AGERE! 2013: Proceedings of the 2013 workshop on Programming based on actors, agents, and decentralized control

Pages 25 - 36

https://doi.org/10.1145/2541329.2541335

Published: 27 October 2013 Publication History

Abstract

Although timed actor-based models attracted more attention in the recent years, there is not much done on analyzing and model checking of such systems. The actor based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints, and a supporting tool was developed for automated translation of Timed Rebeca models to Erlang. The translated code can be executed using McErlang. In this paper, we propose extensions for Timed Rebeca language to improve the usability of the language. Designers can now develop models expressing more complex behaviors by calling Erlang custom functions and using lists. Moreover, to be able to use the new version of McErlang which supports timing constructs of Timed Rebeca we changed the mapping and the tool accordingly. This gives us the possibility of model checking and simulation of Timed Rebeca models for the first time. We can use the safety monitors in McErlang to verify safety properties in the model. Also, statistical methods are applied to the simulation results to reason about the system behavior. We examine the typical case study of elevators to show the applicability of our technique and tool.

References

[1]

L. Aceto, M. Cimini, A. Inglfsdttir, A. H. Reynisson, S. H. Sigurdarson, and M. Sirjani. Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca. In FOCLASA'11, pages 1--19, 2011.

[2]

G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1990.

Digital Library

[3]

G. Agha. The Structure and Semantics of Actor Languages. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, pages 1--59. Springer-Verlag, Berlin, Germany, 1990.

Digital Library

[4]

R. Alur and D. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126:183--235, 1994.

Digital Library

[5]

A. H. Buss. Modeling with Event Graphs. In Proceedings of the 28th conference on winter simulation, pages 153--160, 1996.

Digital Library

[6]

C. B. Earle and L. Fredlund. Verification of Timed Erlang Programs Using McErlang. In Proceedings of the 14th joint IFIP WG 6.1 international conference and Proceedings of the 32nd IFIP WG 6.1 international conference on Formal Techniques for Distributed Systems, FMOODS'12/FORTE'12, pages 251--267, Berlin, Heidelberg, 2012. Springer-Verlag. ISBN 978-3-642-30792-8. URL http://dx.doi.org/10.1007/978-3-642-30793-5_16.

Digital Library

[7]

L.-Å. Fredlund and H. Svensson. McErlang: A Model Checker For a Distributed Functional Programming Language. SIGPLAN Not., 42(9):125--136, 2007. ISSN 0362-1340.

Digital Library

[8]

I. Gupta, B. Cho, M. R. Rahman, T. Chajed, C. L. Abad, N. Roberts, and P. Lin. Natjam: Eviction Policies For Supporting Priorities and Deadlines in Mapreduce Clusters. 2009. URL https://www.ideals.illinois.edu/handle/2142/44871.

[9]

C. Hewitt. Description and Theoretical Analysis (Using Schemata) of PLANNER: A Language for Proving Theorems and Manipulating Models in a Robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science, MIT, Apr. 1972.

[10]

M. M. Jaghoori, M. Sirjani, M. R. Mousavi, E. Khamespanah, and A. Movaghar. Symmetry and Partial Order Reduction Techniques in Model Checking Rebeca. Acta Informaticae, 47(1):33--66, 2009.

Digital Library

[11]

E. Khamespanah, Z. Sabahi Kaviani, R. Khosravi, M. Sirjani, and M.-J. Izadi. Timed-rebeca Schedulability and Deadlockfreedom Analysis Using Floating-time Transition System. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! '12, pages 23--34, New York, NY, USA, 2012. ACM. ISBN 978-1-4503-1630-9. URL http://doi.acm.org/10.1145/2414639.2414645.

Digital Library

[12]

H. Kristinsson. Event-based Analysis of Real-Time Actor Models - Master Thesis, Reykjavik University, Iceland, 2012.

[13]

L. Lamport. Real-Time Model Checking is Really Simple. In Proceedings of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification Methods, CHARME'05, pages 162--175, Berlin, Heidelberg, 2005. Springer-Verlag. ISBN 3-540-29105-9, 978-3-540-29105-3. URL http://dx.doi.org/10.1007/11560548_14.

Digital Library

[14]

L. Linderman, K. Mechitov, and B. F. Spencer. TinyOSbased Real-Time Wireless Data Acquisition Framework for Structural Health Monitoring and Control. Structural Control and Health Monitoring, 20(6):10071020, June 2013.

[15]

I. A. Mason and C. L. Talcott. Actor Languages: Their Syntax, Semantics, Translation, and Equivalence. Theoretical Computer Science, 220(2):409--467, June 1999. ISSN 0304-3975. URL http://www.elsevier.com/cas/tree/store/tcs/sub/1999/220/2/3170.pdf.

Digital Library

[16]

P. C. Ö lveczky and J. Meseguer. Semantics and Pragmatics of Real-Time Maude. Higher Order Symbol. Comput., 20(1-2):161--196, June 2007. ISSN 1388-3690. URL http://dx.doi.org/10.1007/s10990-007-9001-5.

Digital Library

[17]

G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, Sept. 1981.

[18]

Rebeca. Rebeca homepage. http://www.rebeca-lang.org.

[19]

S. Ren and G. Agha. RT-synchronizer: Language Support for Real-Time Specifications in Distributed Systems. In Workshop on Languages, Compilers and Tools for Real-Time Systems, pages 50--59, 1995.

Digital Library

[20]

Z. Sharifi, S. Mohammadi, and M. Sirjani. Comparison of NoC Routing Algorithms Using Formal Methods. To be published in proceedings of PDPTA'13, 2013.

[21]

Z. Sharifi, M. Mosaffa, S. Mohammadi, and M. Sirjani. Functional and Performance Analysis of Network-on-Chips Using Actor-based Modeling and Formal Verification. To be published in proceedings of AVOCS'13, 2013.

[22]

J. S. Simonoff. Smoothing Methods in Statistics. Springer, 1998. ISBN 978-0-387-94716-7.

[23]

M. Sirjani and M. M. Jaghoori. Formal Modeling. chapter Ten Years of Analyzing Actors: Rebeca Experience, pages 20--56. Springer-Verlag, Berlin, Heidelberg, 2011. ISBN 978-3-642-24932-7. URL http://dl.acm.org/citation.cfm?id=2074591.2074596.

Digital Library

[24]

M. Sirjani, A. Movaghar, A. Shali, and F. de Boer. Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models. Journal of Universal Computer Science, 11(6):1054--1082, 2005.

[25]

M. Sirjani, A. Movaghar, A. Shali, and F. de Boer. Modeling and Verification of Reactive Systems using Rebeca. Fundamenta Informatica, 63(4):385--410, Dec. 2004.

Digital Library

[26]

UPPAAL. UPPAAL Homepage. http://www.uppaal.com.

Cited By

Hristov MBieniusa AFernandez-Reyes KVoinea A(2024)Erla⁺: Translating TLA⁺ Models into Executable Actor-Based ImplementationsProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678190(13-23)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678190
(2016)Statistical model checking of Timed Rebeca modelsComputer Languages, Systems and Structures10.1016/j.cl.2016.01.00445:C(53-79)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1016/j.cl.2016.01.004
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

Index Terms

Analysing timed Rebeca using McErlang
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
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Recent improvements to the McErlang model checker
ERLANG '09: Proceedings of the 8th ACM SIGPLAN workshop on ERLANG

In this paper we describe a number of recent improvements to the McErlang model checker, including a new source to source translation to enable more Erlang programs to work under McErlang, a methodology for writing properties that can be verified by ...
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 ...
A Case Study on Verifying a Supervisor Component Using McErlang

In this paper we present a work in progress on the formal verification of a process supervisor using the McErlang model checker. The process supervisor is an alternative implementation of the standard supervisor behaviour of Erlang/OTP. This ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

AGERE! 2013: Proceedings of the 2013 workshop on Programming based on actors, agents, and decentralized control

October 2013

156 pages

ISBN:9781450326025

DOI:10.1145/2541329

Program Chairs:
Nadeem Jamali
University of Saskatchewan, Canada
,
Alessandro Ricci
University of Bologna, Italy
,
Gera Weiss
Ben-Gurion University of the Negev, Israel
,
Akinori Yonezawa
Riken -- AICS, Japan

Copyright © 2013 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '13

Sponsor:

SIGPLAN

SPLASH '13: Conference on Systems, Programming, and Applications: Software for Humanity

October 27, 2013

Indiana, Indianapolis, USA

Acceptance Rates

AGERE! 2013 Paper Acceptance Rate 10 of 21 submissions, 48%;

Overall Acceptance Rate 19 of 35 submissions, 54%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
55
Total Downloads

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

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hristov MBieniusa AFernandez-Reyes KVoinea A(2024)Erla⁺: Translating TLA⁺ Models into Executable Actor-Based ImplementationsProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678190(13-23)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678190
(2016)Statistical model checking of Timed Rebeca modelsComputer Languages, Systems and Structures10.1016/j.cl.2016.01.00445:C(53-79)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1016/j.cl.2016.01.004
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

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