A formal approach for translating a SAM architecture to PROMELA Conference

Argote-Garcia, G, Clarke, PJ, He, X et al. (2008). A formal approach for translating a SAM architecture to PROMELA . 440-447.

cited authors

  • Argote-Garcia, G; Clarke, PJ; He, X; Fu, Y; Shi, L

abstract

  • 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.

publication date

  • December 1, 2008

start page

  • 440

end page

  • 447