Abstract
In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The seleptive quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableaux for LTL formulas can be used for selecting either paths or intervals and also for model checking formulas interpreted over paths or intervals.
To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system: Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking.
This research was sponsored in part by the National Science Foundation under grant no. CCR-8722633, by the Semiconductor Research Corporation under contract 92-DJ-294, and by The Defense Advanced Research Projects Agency, Information Science and Technology Office, under the title “Research on Parallel Computing”, ARPA Order No. 7330, issued by DARPA/CMO under Contract MDA972-90-C-0035.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
R. Alur, C. Courcourbetis, and D. Dill. Model-checking for real-time systems. In Symposium on Logic in Computer Science, pages 414–425, 1990.
R. Alur and D. Dill. Automata for modeling real-time systems. In Lecture Notes in Computer Science, 17 th ICALP. Springer-Verlag, 1990.
ANSI Std. FDDI Token Ring Media Access Control, s3t95/83-16 edition, 1986.
M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207–226, 1983.
R. E.Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Symposium on Logic in Computer Science, 1990.
S. Campos, E. Clarke, W. Marrero, and M. Minea. Verus: a tool for quantitative analysis of finite-state real-time systems. In ACM Workshop on Languages Compilers and Tools for Real-Time Systems, 1995.
S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Real-Time Systems Symposium, 1994.
S. V. Campos, E. M. Clarke, W. Marrero, and M. Minea. Timing analysis of industrial real-time systems. In Workshop on Industrial-strength Formal specification Techniques, 1995.
S. Campos, E. Clarke, W. Marrero, and M. Minea. Verifying the performance of the pci local bus using symbolic techniques. In International Conference on Computer Design, 1995.
E. Clarke, O. Grumberg, and H. Hamaguchi. Another look at ltl model checking. In D. Dill, editor, proceedings of the Sixth Conference on Computer-Aided Verification, Lecture Notes in Computer Science 818, pages 415–427. Springer-Verlag, 1994.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981. Springer-Verlag, 1981. Lecture Notes in Computer Science, volume 131.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
P. C. Clements, C. L. Heitmeyer, B. G. Labaw, and A. T. Rose. MT: a toolset for specifying and analyzing real-time systems. In IEEE Real-Time Systems Symposium, 1993.
E.A. Emerson and Chin Laung Lei. Modalities for model checking: Branching time strikes back. Twelfth Symposium on Principles of Programming Languages, January 1985.
A. N. Fredette and R. Cleaveland. RTSL: a language for real-time schedulability analysis. In IEEE Real-Time Systems Symposium, 1993.
T. A. Henzinger, P. H. Ho, and H. Wong-Toi. HyTech: the next generation. In IEEE Real-Time Systems Symposium, 1995.
IEEE Standard Board and American National Standards Institute. Standard Backplane Bus Specification for Multiprocessor Architectures: Futurebus+, ansi/ieee std 896,1 edition, 1990.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th Conference on Principle of Programming languages, 1985.
O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Proc. Conf. Logics of Programs, Lecture Notes in Computer Science 193, pages 196–218. Springer-Verlag, 1985.
Z. Manna and A. Pnueli. The anchored version of the temporal framework. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354, pages 201–284. Springer-Verlag, 1989.
K. L. McMillan. Symbolic model checking — an approach to the state explosion problem. PhD thesis, SCS, Carnegie Mellon University, 1992.
X. Nicollin, J. Sifakis, and S. Yovine. From atp to timed graphs and hybrid systems. In Lecture Notes in Computer Science, Real-Time: Theory in Practice. Springer-Verlag, 1992.
A. Pnueli. The temporal semantics of concurrent programs. In Proceedings of the eighteenth conference on Foundation of Computer Science, 1977.
Y. Ramakrishna, P. Melliar-Smith, L. Moser, L. Dillon, and G. Kutty. Really visual temporal reasoning. In IEEE Real-Time Systems Symposium, 1993.
L. Sha, R. Rajkumar, and S. Sathaye. Generalized rate-monotonic scheduling theory: a framework for developing real-time systems. In Proceedings of the IEEE, Jan 1994.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification.In Proceedings of the First Symposium on Logic in Computer Science, 1986.
F. Wang. Timing behavior analysis for real-time systems. In Proceedings of the Tenth Symposium on Logic in Computer Science, 1995.
J. Yang, A. Mok, and F. Wang. Symbolic model checking for event-driven real-time systems. In IEEE Real-Time Systems Symposium, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Campos, S., Grumberg, O. (1996). Selective quantitative analysis and interval model checking: Verifying different facets of a system. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_74
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_74
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive