In the past decade, software architecture research has mainly focused on the concept formulation and the development of various architecture description languages. This field has matured enough and thus requires more emphasis on validation techniques. Symbolic model checking has been a highly successful automatic validation technique for hardware systems. We are interested in whether symbolic model checking can be effectively applied to software architecture validation. In this paper, we present our approach to apply the symbolic model checking technique to verify software architecture specifications written in SAM. Copyright 2002 ACM.
