Timing analysis in COSPAN | Springer Nature Link
Advertisement
Timing analysis in COSPAN
Conference paper
First Online:
01 January 2005
pp 220–231
Cite this conference paper
Hybrid Systems III
(HS 1995)
Abstract
We describe how to model and verify real-time systems using the formal verification tool
Cospan
. The verifier supports automata-theoretic verification of coordinating processes with timing constraints. We discuss different heuristics, and our experiences with the tool for certain benchmark problems appearing in the verification literature.
This is a preview of subscription content,
log in via an institution
to check access.
Access this chapter
Log in via an institution
Institutional subscriptions
Preview
Unable to display preview.
Download preview
PDF.
Unable to display preview.
Download preview
PDF.
Similar content being viewed by others
Automated Verification for Real-Time Systems
Chapter
Unified Timing-Aware Program Verification
Chapter
Timed Contract Automata
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Logical Analysis
Formal Languages and Automata Theory
Formal Logic
Technical Languages
Systems Analysis
Electronics Design and Verification
References
R. Alur, C. Courcoubetis, and D.L. Dill. Model-checking in dense real-time.
Information and Computation
, 104(1):2–34, 1993.
Article
Google Scholar
R. Alur, C. Courcoubetis, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems.
Theoretical Computer Science
, 138:3–34, 1995.
Article
Google Scholar
R. Alur and D.L. Dill. A theory of timed automata.
Theoretical Computer Science
, 126:183–235, 1994.
Article
Google Scholar
R. Alur and T.A. Henzinger. A really temporal logic.
Journal of the ACM
, 41(1):181–204, 1994.
Article
Google Scholar
R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation.
Information and Computation
, 118(1):142–157, 1995.
Google Scholar
B. Berthomieu and M. Diaz. Modeling and verification of time-dependent systems using time Petri nets.
IEEE Transactions on Software Engineering
, SE-17(3):259–273, 1991.
Article
Google Scholar
F. Balarin and A. Sangiovanni-Vincentelli. A verification strategy for timing-constrained systems. In
Proceedings of the Fourth Workshop on Computer-Aided Verification
, LNCS 663, pages 151–163. Springer-Verlag, 1992.
Google Scholar
J.R. Burch. Combining CTL, trace theory and timing models. In
Automatic Verification Methods for Finite State Systems: Proceedings of the First CAV
, LNCS 407, pages 197–212. Springer-Verlag, 1989.
Google Scholar
D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor,
Automatic Verification Methods for Finite State Systems
, LNCS 407, pages 197–212. Springer-Verlag, 1989.
Google Scholar
C. Daws, A. Olivero, and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In
Formal Description Techniques VII, Proceedings of FORTE'94
, pages 227–242, 1994.
Google Scholar
T.A. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In
ICALP 92: Automata, Languages, and Programming
, LNCS 623, pages 545–558. Springer-Verlag, 1992.
Google Scholar
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems.
Information and Computation
, 111(2):193–244, 1994.
Article
Google Scholar
R.P. Kurshan.
Computer-aided Verification of Coordinating Processes: the automata-theoretic approach
. Princeton University Press, 1994.
Google Scholar
K. Larsen, P. Pettersson, and W. Yi. Compositional and symbolic model-checking of real-time systems. In
Proceedings of the 16th IEEE Real-Time Systems Symposium
, 1995.
Google Scholar
K. McMillan.
Symbolic model checking: an approach to the state explosion problem
. Kluwer Academic Publishers, 1993.
Google Scholar
A. Puri and P. Varaiya. Verification of hybrid systems using abstractions. In
Hybrid Systems II
, LNCS 999. Springer-Verlag, 1995.
Google Scholar
T. Rokicki.
Representing and modeling digital circuits
. PhD thesis, Stanford University, 1993.
Google Scholar
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor,
Handbook of Theoretical Computer Science
, volume B, pages 133–191. Elsevier Science Publishers, 1990.
Google Scholar
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In
Proceedings of the First IEEE Symposium on Logic in Computer Science
, pages 332–344, 1986.
Google Scholar
H. Wong-Toi.
Symbolic approximations for verifying real-time systems
. PhD thesis, Stanford University, 1994.
Google Scholar
Download references
Author information
Authors and Affiliations
AT&T Bell Laboratories, Murray Hill
Rajeev Alur & Robert P. Kurshan
Authors
Rajeev Alur
View author publications
Search author on:
PubMed
Google Scholar
Robert P. Kurshan
View author publications
Search author on:
PubMed
Google Scholar
Editor information
Rajeev Alur Thomas A. Henzinger Eduardo D. Sontag
Rights and permissions
Reprints and permissions
Copyright information
About this paper
Cite this paper
Alur, R., Kurshan, R.P. (1996). Timing analysis in COSPAN.

In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020948
Download citation
.RIS
.ENW
.BIB
DOI
Published
10 June 2005
Publisher Name
Springer, Berlin, Heidelberg
Print ISBN
978-3-540-61155-4
Online ISBN
978-3-540-68334-6
eBook Packages
Springer Book Archive
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Mutual Exclusion
Timing Assignment
Reachable State
Acceptance Condition
Timing Verification
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Publish with us
Policies and ethics
Access this chapter
Log in via an institution
Institutional subscriptions