Translating Software Designs for Model Checking

Abstract. This paper presents a systematic consideration of the major issues involved in translation of executable design level software specification languages to directly model-checkable formal languages. These issues are considered under the framework of integrated model/property translation and include: (1) translator architecture; (2) semantics translation from a software language to a formal language; (3) property specification and translation; (4) transformations for state space reduction; (5) translator validation and evolution. Solutions to these issues are defined, described, and illustrated in the context of translating xUML, an executable design level software specification language, to S/R, the input formal language of the COSPAN model checker.

• Type: Conference
• Year: 2004
• Where: FASE
• Authors: Fei Xie, Vladimir Levin, Robert P. Kurshan, James C. Browne
• Keywords: FASE 2004, Formal Language, Level Software Specification, Software Engineering, Software Specification Language