Abstract
In this paper, we present a comprehensive approach to model check- ing component-based systems (including software, hardware, and embedded systems) through abstraction and refinement. This approach is based on assume-guarantee compositional reasoning and features two synergistic techniques: (1) an automatic algorithm to component-based abstraction and (2) a mechanized assistant for abstraction refinement. The key insight to the abstraction algorithm is that a verified property is a natural abstraction of a component. The abstraction algorithm automatically determines which component properties can be included in the abstraction for verifying a system property by determining whether the assumptions of the component properties hold in the context of the system. If the abstraction fails to establish the system property, the refinement assistant determines the causes of the failure, e.g., why a component property is not included, and provides automatic remedies or requests manual remedies. This approach has been applied in component-based hardware/software co-verification of embedded systems. Case studies have shown that this approach is very effective in abstracting component-based embedded systems and guiding abstraction refinement.
This research was supported by Semiconductor Research Corporation Contract 1356.001 and National Science Foundation Grant 0720546.
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
Jacome, M.F., Peixoto, H.P.: A survey of digital design reuse. IEEE Design and Test of Computers 18(3) (2001)
Szyperski, C.: Component Software - Beyond Object-Oriented Programming. Addison-Wesley, Reading (2002)
Maliniak, D.: Assertion-based verification smooths the road to IP reuse. Electronic Design (September 2002)
IEEE: IEEE Property Specification Language (PSL) (IEEE Std 1850-2005). IEEE (2005)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)
de Roever, W.P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge University Press, Cambridge (2001)
Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transaction on Software Engineering 7(4) (1981)
Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)
Abadi, M., Lamport, L.: Conjoining specifications. TOPLASÂ 17(3) (1995)
Alur, R., Henzinger, T.: Reactive modules. FMSDÂ 15(1) (1999)
McMillan, K.L.: A methodology for hardware verification using compositional model checking. Cadence Design Systems Technical Reports (1999)
Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.: Assume-guarantee based compositional reasoning for synchronous timing diagrams. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031. Springer, Heidelberg (2001)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Hardin, R.H., Har’El, Z., Kurshan., R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Xie, F., Yang, G., Song, X.: Compositional reasoning for hardware/software co-verification. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218. Springer, Heidelberg (2006)
Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters 21(4) (1985)
Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)
IEEE: IEEE Standard for Verilog (IEEE Std 1364-2005). IEEE (2005)
Xie, F., Yang, G., Song, X.: Component-based hardware/software co-verification. In: Proc. of MEMOCODE (2006)
Xie, F., Song, X., Chung, H., Nandi, R.: Translation-based co-verification. In: Proc. of MEMOCODE (2005)
Kurshan, R.P.: FormalCheck User Manual. Cadence (1998)
Xie, F., Levin, V., Browne, J.C.: Objectcheck: A model checking tool for executable object-oriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306. Springer, Heidelberg (2002)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, J., Sun, X., Xie, F., Song, X. (2008). Component-Based Abstraction and Refinement. In: Mei, H. (eds) High Confidence Software Reuse in Large Systems. ICSR 2008. Lecture Notes in Computer Science, vol 5030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68073-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-68073-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68062-8
Online ISBN: 978-3-540-68073-4
eBook Packages: Computer ScienceComputer Science (R0)