A toolsuite for the verification of real-time systems in Eclipse
Authors: 
Lucía Cavatorta, 
Guido de Caso, Andrés Ferrari, Víctor Braberman, 
Diego Garbervetsky, Nicolás Kicillof, Fernando Schapachnik, Alfredo OliveroAuthors Info & Claims
Lucía Cavatorta, Guido de Caso, Andrés Ferrari, Víctor Braberman, Diego Garbervetsky, Nicolás Kicillof, Fernando Schapachnik, Alfredo OliveroAuthors Info & ClaimsPages 35 - 39
Abstract
In this work we present an Eclipse plug-in for the VINTIME (Verifier of INtegrated TImed ModEls) suite of tools that combines high-level expressive power, unassisted property-preserving model reduction and distributed model checking to describe and verify complex real-time system designs and their properties.
References
[1]
A. Alfonso, V. Braberman, N. Kicillof, and A. Olivero. Visual timed event scenarios. In Proc. of the 26th ACM/IEEE International Conference on Software Engineering. ACM Press, 2004.
[2]
A. Alfonso, D. Garbervetsky, V. Braberman, A. Olivero, N. Kicillof, and F. Schapachnik. Vintime: Combining high-level finesse with low-level muscle to verify real-time systems. In First International Conference on Principles of Software Engineering, PRISE 2004, Buenos Aires, Argentina, November 2004.
[3]
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183--235, 1994.
[4]
J. Bengtsson, K. Guldstrand Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL - a tool suite for automatic verification of real-time systems. In Hybrid Systems, pages 232--243. Springer-Verlag, 1995.
[5]
V. Braberman. Modeling and Checking Real-Time Systems Designs. Ph d. thesis, Departmento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, 2000.
[6]
V. Braberman and M. Felder. Verification of real-time designs: Combining scheduling theory with automatic formal verification. In Software Engineering - ESEC/FSE'99: 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1687 of LNCS, pages 521--525, Touluse, France, September 1999. Springer-Verlag.
[7]
V. Braberman, D. Garbervetsky, and A. Olivero. ObsSlice: A timed automata slicer based on observers. In Proc. of the 16th Intl. Conf. CAV '04, LNCS. Springer Verlag, 2004.
[8]
V. Braberman, N. Kicillof, and A. Olivero. A scenario-matching approach to the description and model checking of real-time properties. IEEE Transactions on Software Engineering, 31(12):1028--1041, 2005.
[9]
V. Braberman, A. Olivero, and F. Schapachnik. Zeus: A distributed timed model checker based on Kronos. In 1stWorkshop on Parallel and Distributed Model Checking, affiliated to CONCUR 2002 (13thInternational Conference on Concurrency Theory), volume 68 of ENTCS, Brno, Czech Republic, August 2002. Elsevier.
[10]
V. Braberman, A. Olivero, and F. Schapachnik. Issues in Distributed Model-Checking of Timed Automata: building ZEUS. International Journal of Software Tools for Technology Transfer, 7:4--18, feb 2005.
[11]
V. Braberman, A. Olivero, and F. Schapachnik. Dealing with practical limitations of distributed timed model checking. Formal Methods in System Design, 2006.
[12]
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with KRONOS. In Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS'95), pages 66--75, Pisa, Italy, December 1995. IEEE Computer Society Press.
[13]
M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In O. Grumberg, editor, Proceedings of the 9thInternational Conference on Computer Aided Verification (CAV'97), volume 1254 of LNCS, pages 179--190, Israel, June 1997. Springer-Verlag.
[14]
B. Selic, A. Moore, M. Woodside, B. Watson, M. Bjorkander, M. Gerhardt, and D. Petriu. UML Profile for Schedulability, Performance and Time Specification. Object Management Group, 2005.
[15]
S. Tripakis. L'Analyse Formelle des Systemès Temporisés en Practique. PhD thesis, Université Joseph Fourier, 1998.
[16]
S. Tripakis and S. Yovine. Verification of the fast reservation protocol with delayed transmission using the tool KRONOS. In Proceedings of the 4thIEEE Real-Time Technology and Applications Symposium (RTAS'98), pages 165--170, Denver, Colorado, USA, June 1998. IEEE Computer Society Press.
Index Terms
- A toolsuite for the verification of real-time systems in Eclipse
Recommendations
Verification of real-time systems design
The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this ...
Efficient and User-Friendly Verification
A compositional verification method from a high-level resource-management standpoint is presented for dense-time concurrent systems and implemented in the tool of SGM (State-Graph Manipulators) with graphical user interface. SGM packages sophisticated ...
Formal Analysis and Verification of a Multimedia Messaging Service Protocol
CSO '11: Proceedings of the 2011 Fourth International Joint Conference on Computational Sciences and Optimizationthis paper reports about the formal analysis and verification of a Multimedia Messaging Service Protocol (MMS) used by NOKIA in its products. We started with the Timed Automata models of the MMS protocol, and then we performed verifications by model-...
Comments
Information & Contributors
Information
Published In
October 2006
93 pages
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
- IBM: IBM
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 22 October 2006
Check for updates
Author Tags
Qualifiers
- Article
Acceptance Rates
eclipse '06 Paper Acceptance Rate 17 of 30 submissions, 57%;
Overall Acceptance Rate 38 of 79 submissions, 48%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 182Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 08 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in