research-article

Automatically transforming and relating Uppaal models of embedded systems

Authors:

Timothy Bourke,

Arcot SowmyaAuthors Info & Claims

EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

Pages 59 - 68

https://doi.org/10.1145/1450058.1450068

Published: 19 October 2008 Publication History

Get Access

Abstract

Relations between models are important for effective automatic validation, for comparing implementations with specifications, and for increased understanding of embedded systems designs. Timed automata may be used to model a system at multiple levels of abstraction, and timed trace inclusion is one way to relate the models.

It is known that a deterministic and Τ-free timed automaton can be transformed such that reachability analysis can decide timed trace inclusion with another timed automaton. Performing the transformation manually is tedious and error-prone. We have developed a tool that does it automatically for a large subset of Uppaal models.

Certain features of the Uppaal modeling language, namely selection bindings and channel arrays, complicate the transformation. We formalize these features and extend the validation technique to incorporate them. We find it impracticable to manipulate some forms of channel array subscripts, and some combinations of selection bindings and universal quantifiers; doing so either requires premature parameter instantiation or produces models that Uppaal rejects.

References

[1]

R. Alur and D. L. Dill. A theory of timed automata. Theoretical Comp. Sci., 126(2):183--235, Apr. 1994.

Digital Library

Google Scholar

[2]

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information & Computation, 111(2):192--244, June 1994.

Digital Library

Google Scholar

[3]

H. E. Jensen, K. G. Larsen, and A. Skou. Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In M. Joseph, editor, Proc. 6th Int. Symp. Formal Techniques for Real-Time and Fault-Tolerance, volume 1926 of LNCS, pages 19--30, Pune, India, Sept. 2000. Springer-Verlag.

Digital Library

Google Scholar

[4]

K. G. Larsen, P. Pettersson, and Y. Wang. Uppaal in a nutshell. Int. J. Software Tools for Technology Transfer, 1(1-2):134--152, Oct. 1997.

Digital Library

Google Scholar

[5]

N. Lynch and F. Vaandrager. Forward and backward simulations. Part I: Untimed systems. Information & Computation, 121(2):214--233, Sept. 1995.

Digital Library

Google Scholar

[6]

N. Lynch and F. Vaandrager. Forward and backward simulations. Part II: Timing-based systems. Information & Computation, 128(1):1--25, July 1996.

Digital Library

Google Scholar

[7]

M. I. Stoelinga. Alea Jacta est: Verification of probabilistic, real-time and parametric systems. PhD thesis, Katholieke Universiteit Nijmegen, Apr. 2002.

Google Scholar

[8]

Y. Wang, P. Pettersson, and M. Daniels. Automatic verification of real-time communicating systems by constraint-solving. In D. Hogrefe and S. Leue, editors, Formal Description Techniques VII, pages 223--238, Berne, Switzerland, 1994. IFIP, Chapman & Hall.

Digital Library

Google Scholar

Cited By

View all

Rehfeld SLatoschik MTramberend H(2016)Estimating latency and concurrency of asynchronous real-time interactive systems using model checking2016 IEEE Virtual Reality (VR)10.1109/VR.2016.7504688(57-66)Online publication date: Mar-2016
https://doi.org/10.1109/VR.2016.7504688
David ALarsen KLegay ANyman UTraonouez LWąsowski A(2015)Real-time specificationsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0286-x17:1(17-45)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1007/s10009-013-0286-x
Bourke TSowmya A(2013)Analyzing an embedded sensor with timed automata in uppaalACM Transactions on Embedded Computing Systems10.1145/2539036.253904013:3(1-26)Online publication date: 24-Dec-2013
https://dl.acm.org/doi/10.1145/2539036.2539040
Show More Cited By

Index Terms

Automatically transforming and relating Uppaal models of embedded systems
1. Computer systems organization
  1. Embedded and cyber-physical systems
  2. Real-time systems
2. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation

Recommendations

Verification of dynamically reconfigurable embedded systems by model transformation rules
CODES/ISSS '10: Proceedings of the eighth IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis

This paper describes a methodology for the verification of reconfigurable embedded systems. The reconfigurable systems are described by means of the Reconfigurable Discrete Event Specified System (RecDEVS) computational model and the verification is ...
Analyzing an embedded sensor with timed automata in uppaal

An infrared sensor is modeled and analyzed in Uppaal. The sensor typifies the sort of component that engineers regularly integrate into larger systems by writing interface hardware and software.

In all, three main models are developed. In the first ...
UPPAAL-Based Software-Defined Network Verification
TMPA '13: Proceedings of the 2013 Tools & Methods of Program Analysis

A lot of efforts were made in the last few years in the area of software-defined networks (SDN) - a special kind of computer networks in which the switching device control is fully centralized. This paper investigates the problems of formal description ...

Comments

Information & Contributors

Information

Published In

EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

October 2008

284 pages

ISBN:9781605584683

DOI:10.1145/1450058

Program Chairs:
Luca de Alfaro
University of California, Santa Cruz
,
Jens Palsberg
University of California, Los Angeles

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: 19 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESWEEK 08

Sponsor:

ESWEEK 08: Fourth Embedded Systems Week

October 19 - 24, 2008

GA, Atlanta, USA

Acceptance Rates

Overall Acceptance Rate 60 of 203 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
266
Total Downloads

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

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Rehfeld SLatoschik MTramberend H(2016)Estimating latency and concurrency of asynchronous real-time interactive systems using model checking2016 IEEE Virtual Reality (VR)10.1109/VR.2016.7504688(57-66)Online publication date: Mar-2016
https://doi.org/10.1109/VR.2016.7504688
David ALarsen KLegay ANyman UTraonouez LWąsowski A(2015)Real-time specificationsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0286-x17:1(17-45)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1007/s10009-013-0286-x
Bourke TSowmya A(2013)Analyzing an embedded sensor with timed automata in uppaalACM Transactions on Embedded Computing Systems10.1145/2539036.253904013:3(1-26)Online publication date: 24-Dec-2013
https://dl.acm.org/doi/10.1145/2539036.2539040
Bourke TDavid ALarsen KLegay ALime DNyman UW$#261;sowski A(2010)New results on timed specificationsProceedings of the 20th international conference on Recent Trends in Algebraic Development Techniques10.1007/978-3-642-28412-0_12(175-192)Online publication date: 1-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-28412-0_12

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

Verification of dynamically reconfigurable embedded systems by model transformation rules

Analyzing an embedded sensor with timed automata in uppaal

UPPAAL-Based Software-Defined Network Verification

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

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