Abstract
Software is being developed from off-the-shelf third party components. The interface specification of such a component may be under specified or may not fully match the user requirement. In this paper, we address the problem of customizing such components to particular users. We achieve this by constructing a monitor that monitors the component and detects any bad behaviors.
Construction of such monitors essentially involves synthesizing safety properties that imply a given property that is obtained from the interface specifications of the component and the goal specification of the user. We present various methods for synthesizing such safety properties when the given property is given by an automaton or a temporal logic formula. We show that our methods are sound and complete. These results are extensions of the results given in [11].
This work is supported in part by the NSF grants CCR-9988884 and CCR-0205365.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: The existence of state mappings. In: Proceedings of the ACM Symposium on Logic in Computer Science (1988)
Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Emerson, E.A., Sistla, A.P.: Triple exponential decision procedure for the logic CTL*. In: Workshop on the Logics of Program. Carnegie-Mellon University (1983)
Hungar, H., Steffen, B.: Behavior-based model construction. STTT 6(1), 4–14 (2004)
Jonsson, B.: Compositional verification of distributed systems. In: Proceedings of the 6th ACM Symposium on Principles of Distributed Computing (1987)
Lamport, L.: Logical foundation, distributed systems- methods and tools for specification. In: Alford, M.W., Hommel, G., Schneider, F.B., Ansart, J.P., Lamport, L., Mullery, G.P., Liskov, B. (eds.) Distributed Systems. LNCS, vol. 190. Springer, Heidelberg (1985)
Larsen, K.: Ideal specification formalisms = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458. Springer, Heidelberg (1990)
Larsen, K.: The expressive power of implicit specifications. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510. Springer, Heidelberg (1991)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. Princ. of Prog. Lang., pp. 97–107 (1985)
Margaria, T., Raffelt, H., Steffen, B.: Knowledge-based relevance filtering for efficient system-level test-based model generation (to appear). Springer, Heidelberg; nnovations in Systems and Software Engineering. A NASA Journal. Springer, Heidelberg
Margaria, T., Sistla, A., Steffen, B., Zuck, L.D.: Taming interface specifications. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 548–561. Springer, Heidelberg (2005)
Margaria, T., Sistla, A., Steffen, B., Zuck, L.D.: Taming interface specifications (2005), www.cs.uic.edu/~sistla
Pnueli, A., Zaks, A., Zuck, L.D.: Monitoring interfaces for faults. In: Proceedings of the 5th Workshop on Runtime Verification, RV 2005 (2005) To appear in a special issue of ENTCS
Safra, S.: On the complexity of ù-automata. In: 29th annual Symposium on Foundations of Computer Science, White Plains, New York, October 24–26, pp. 319–327. IEEE Computer Society Press, Los Alamitos (1988)
Sistla, A., Zhou, M., Zuck, L.D.: Monitoring off-the-shelf components. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 222–236. Springer, Heidelberg (2005)
Sistla, A.P.: On characterization of safety and liveness properties in temporal logic. In: Proceedings of the ACM Symposium on Principle of Distributed Computing (1985)
Sistla, A.P.: Proving correctness with respect to nondeterministic safety specifications. Information Processing Letters 39, 45–49 (1991)
Vardi, M., Wolper, P., Sistla, A.P.: Reasoning about infinite computations. In: Proceedings of IEEE Symposium on Foundations of Computer Science (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sistla, A.P., Zhou, M., Zuck, L.D. (2005). Monitoring Off-the-Shelf Components. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_15
Download citation
DOI: https://doi.org/10.1007/11609773_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31139-3
Online ISBN: 978-3-540-31622-0
eBook Packages: Computer ScienceComputer Science (R0)