With the inevitable increase in complexity of both hardware and software systems, there is a growing demand for methodologies that can increase confidence in correct system design and construction. Such methodologies will result in improved quality, as well as in a reduction to the total development cost of a system. Our main goal is the development of practical and effective techniques to support for analyzing the behavior of complex systems. More specifically, we focus on model checking method that can be easily introduced into the system development process Software Architecture Methodology (SAM). We chose symbolic model checking method to verify complex software systems, so the verification procedure is automated. In this thesis, our works include: 1. Design a global method for checking SAM software architecture model. 2 Present a compositional model checking method for SAM software architecture methodology. 3. Implement a system to translate SAM model into Symbolic Model Verifier (SMV) model automatically. 4. Prove the correctness of the translation method. Using the compositional model checking method, we check some properties such as reachability and deadlock in a Flexible Manufacturing System (FMS) which is modeled using SAM, and we improve the previous model through the help of the counter example produced from the checking system.
