Abstract: During the last decade, Model Checking has proven its efficacy and powerin circuit design, network protocol analysis and bug hunting. Recentresearch on automatic verification has shown that no singlemodel-checking technique has the edge over all others in allapplication areas. So, it is very difficult to determinewhich technique is the most suitable for a given model. It is thussensible to apply different techniques to the same model. However,this is a very tedious and time-consuming task, for each algorithmuses its own description language. Applying Model Checking insoftware design and verification has been proved very difficult.Software architectures (SA) are engineering artifacts that providehigh-level and abstract descriptions of complex software systems.In this paper a Direct Model Checking (DMC) methodbased on Kripke Structure and Matrix Algorithm is provided. Combined andintegrated with domain specific software architecture descriptionlanguages (ADLs), DMC can be used for computing consistency andother critical properties.