An approach to validating translation correctness from SAM to Java

An approach to validating translation correctness from SAM to Java Conference

Fu, Y, Dong, Z, Argote-Garcia, G et al. (2007). An approach to validating translation correctness from SAM to Java . 45-50.

SAM is a formal software architecture description model based on Petri nets and temporal logic. SAM Parser is a tool to automatically translate a SAM architecture design into a program in ArchJava/Java/AspectJ with run-time verification capability. In this paper, we present an approach to show the correctness of the translation algorithm implemented in SAM Parser. Our approach requires a restricted Petri net model with an interleaving semantics, defines the operational semantics of a Java program using communication traces, and shows the consistency between an execution sequence of a Petri net and a communication trace of the corresponding Java program. Copyright © (2007) by Knowledge Systems Institute (KSI).