Article

Free access

Abstraction from counters: an application on real-time systems

Authors:

G. Logothetis,

K. SchneiderAuthors Info & Claims

DATE '00: Proceedings of the conference on Design, automation and test in Europe

Pages 486 - 493

https://doi.org/10.1145/343647.343828

Published: 01 January 2000 Publication History

PDF eReader Publisher Site

References

[1]

R. Alur and D. Dill. Automata for modelling real-time systems. Theoretical Computer Science, 126(2): 183-236, April 1994.

Digital Library

Google Scholar

[2]

J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL in 1995. In ln Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in Lecture Notes In Computer Science, pages 431-434. Springer-Verlag, March 19956.

Digital Library

Google Scholar

[3]

J. Burch, E. Clarke, K. McMillan, and D. Dill. Sequential Circuit Verification Using Symbolic Model Checking. In ACM/IEEE Design Automation Conference (DAC), pages 46-51, Los Alamitos, CA, June 1990. ACM/IEEE, IEEE Society Press.

Digital Library

Google Scholar

[4]

G. Cabodi, P. Camurati, L. Lavagno, and S. Quer. Verification and synthesis of counters based on symbolic techniques. In European Design and Test Conference (EDTC), pages 176-181, Paris, France, March 1997. IEEE Computer Society Press.

Digital Library

Google Scholar

[5]

S. Campos, E. Clarke, W. Marrero, and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. Technical Report CMU-CS-96-147, June 1996. ftp ://reports.adm.c s.cmu.edu/usr/anon/1996/CMU- CS-96-147.ps.

Google Scholar

[6]

S. Campos, E. Clarke, W. Marrero, and M. Minea. Verus: A tool for quantitative analysis of finite-state real-time systems. Technical Report CMU-CS-96-159, August 1996.

Google Scholar

[7]

E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and systems, 16(5): 1512-1542, September 1994.

Digital Library

Google Scholar

[8]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symposium on Principles of Programming Languages (POPL), pages 238-252. ACM, 1977.

Digital Library

Google Scholar

[9]

D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS), 1997.

Digital Library

Google Scholar

[10]

C. Daws, A. Olivero, and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In In Proc. of 7th International Conference on Formal Description Techniques, 1994.

Digital Library

Google Scholar

[11]

C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS' 98, 1998.

Digital Library

Google Scholar

[12]

C. Heitmeyer and N. Lynch. The generalize railroad crossing: A case study in formal verification of real-time systems. In Proc. of the IEEE Real-Time Systems Symposium, pages 120-131, San Juan, Puerto Rico, December 1994.

Google Scholar

[13]

P.H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, Conference on Computer Aided Verification (CAV), volume 939 of Lecture Notes in Computer Science, pages 381-394, Liege, Belgium, July 1995. Springer Verlag.

Digital Library

Google Scholar

[14]

S. Krischer. The backward walk approach in FSM verification. In D. Agnew, L. Claesen, and R. Camposano, editors, IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pages 143-150, Ottawa, Canada, April 1993. IFIP WG10.2, CHDL'93, IEEE COMPSOC, Elsevier Science Publishers B.V., Amsterdam, Netherland.

Digital Library

Google Scholar

[15]

K. Kristoffersen, F. Laroussinie, K. Larsen, P. Pettersson, and W. Yi. A compositional proof of a real-time mutual exclusion protocol. In In Proc. of the 7th International Joint Conference on the Theory and Practice of Software Development, 1997.

Digital Library

Google Scholar

[16]

L. Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 1987.

Digital Library

Google Scholar

[17]

A. Loetzbeyer. Temporale Realzeitverifikation. PhD thesis, Universitaet Karlsruhe, March 1999.

Google Scholar

[18]

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal methods in System Design, 6:1-35, February 1995.

Digital Library

Google Scholar

[19]

E. Macii, B. Plessier, and F. Somenzi. Verification of System Containing Counters. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 179-182, Santa Clara, California, November 1992. ACM/IEEE, IEEE Computer Society Press.

Digital Library

Google Scholar

Cited By

View all

Zöbel DZöbel D(2019)EinführungEchtzeitsysteme10.1007/978-3-662-60421-2_1(1-52)Online publication date: 27-Nov-2019
https://doi.org/10.1007/978-3-662-60421-2_1
Seligman ESchubert TKumar M(2015)Dealing with complexityFormal Verification10.1016/B978-0-12-800727-3.00010-1(289-323)Online publication date: 2015
https://doi.org/10.1016/B978-0-12-800727-3.00010-1
Logothetis GSchneider K(2001)Symbolic model checking of real-time systemsProceedings Eighth International Symposium on Temporal Representation and Reasoning. TIME 200110.1109/TIME.2001.930720(214-223)Online publication date: 2001
https://doi.org/10.1109/TIME.2001.930720
Show More Cited By

Index Terms

Abstraction from counters: an application on real-time systems
1. Hardware
  1. Hardware test
  2. Robustness
    1. Hardware reliability
2. Software and its engineering
  1. Software creation and management
    1. Designing software
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems

Recommendations

Adding Approximate Counters
Special Issue: Invited papers from PPoPP 2016, Part 1

We describe a general framework for adding the values of two approximate counters to produce a new approximate counter value whose expected estimated value is equal to the sum of the expected estimated values of the given approximate counters. (To the ...
Adding approximate counters
PPoPP '16

We describe a general framework for adding the values of two approximate counters to produce a new approximate counter value whose expected estimated value is equal to the sum of the expected estimated values of the given approximate counters. (To the ...
Adding approximate counters
PPoPP '16: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

We describe a general framework for adding the values of two approximate counters to produce a new approximate counter value whose expected estimated value is equal to the sum of the expected estimated values of the given approximate counters. (To the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '00: Proceedings of the conference on Design, automation and test in Europe

January 2000

707 pages

ISBN:1581132441

DOI:10.1145/343647

Chairman:
Ivo Bolsens
IMEC, Leuven, Belgium

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: 01 January 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DATE00

Sponsor:

EDAA
EDAC
SIGDA
IEEE-CS
IFIP
The Russian Academy of Sciences

DATE00: Design Automation and Test in Europe

March 27 - 30, 2000

Paris, France

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
165
Total Downloads

Downloads (Last 12 months)26
Downloads (Last 6 weeks)3

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zöbel DZöbel D(2019)EinführungEchtzeitsysteme10.1007/978-3-662-60421-2_1(1-52)Online publication date: 27-Nov-2019
https://doi.org/10.1007/978-3-662-60421-2_1
Seligman ESchubert TKumar M(2015)Dealing with complexityFormal Verification10.1016/B978-0-12-800727-3.00010-1(289-323)Online publication date: 2015
https://doi.org/10.1016/B978-0-12-800727-3.00010-1
Logothetis GSchneider K(2001)Symbolic model checking of real-time systemsProceedings Eighth International Symposium on Temporal Representation and Reasoning. TIME 200110.1109/TIME.2001.930720(214-223)Online publication date: 2001
https://doi.org/10.1109/TIME.2001.930720
Logothetis GSchneider K(2001)A new approach to the specification and verification of real-time systemsProceedings 13th Euromicro Conference on Real-Time Systems10.1109/EMRTS.2001.934025(171-180)Online publication date: 2001
https://doi.org/10.1109/EMRTS.2001.934025

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Adding Approximate Counters

Adding approximate counters

Adding approximate counters