Quality assurance is recognized as a critical aspect in software construction. SAM is a formal software architecture description model that combines Petri Nets and Temporal Logic. PROMELA is the language used in the Spin model checker. This paper presents an approach to translate a restricted SAM model to a PROMELA program, enabling the model checking of the SAM model. We define the translation and show its correctness in terms of completeness and consistency. Completeness establishes that a SAM model maps all of its elements to PROMELA ones; whereas, consistency defines that an execution of a SAM model has a corresponding execution in a PROMELA program. The translation is also implemented as part of our software tool supporting SAM. Some aspects of the tool are discussed.
