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. © Springer-Verlag 2004.
CITATION STYLE
Xie, F., Levin, V., Kurshan, R. P., & Browne, J. C. (2004). Translating Software Designs for Model Checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2984, 324–338. https://doi.org/10.1007/978-3-540-24721-0_24
Mendeley helps you to discover research relevant for your work.