TY - GEN
T1 - Transforming architectural descriptions for formal analysis
AU - Ibrahim, Naseem
AU - Mohammad, Mubarak
AU - Alagar, Vangalur
PY - 2013
Y1 - 2013
N2 - Model transformation is the process of automatically generating a target model from a source model according to a set of transformation rules. Automatic model transformation has the potential to eliminate the complexity, the inconsistencies and faults that are inherent in a manual model transformation process. Many of the existing tools that automate the model transformation process require the encoding of transformation rules within the transformation process, which limits their reuse and usability in different contexts. This paper presents a tool that automates the model transformation of component-based systems specification. The tool takes an architectural specification as input and generates a behavior protocol as output. The transformation rules are described independently from the transformation process. This allows changing the transformation rules without affecting the transformation process. We discuss in detail the transformation rules for transforming a trustworthy component-based system, formally specified in an architecture description language (TADL), to an extended timed automata specification. The goal is to formally verify trustworthiness properties claimed in the source model by model checking the trustworthiness properties in the target model. By varying the target model and the set of transformation rules the same tool can be used to obtain different target models and use different verification techniques.
AB - Model transformation is the process of automatically generating a target model from a source model according to a set of transformation rules. Automatic model transformation has the potential to eliminate the complexity, the inconsistencies and faults that are inherent in a manual model transformation process. Many of the existing tools that automate the model transformation process require the encoding of transformation rules within the transformation process, which limits their reuse and usability in different contexts. This paper presents a tool that automates the model transformation of component-based systems specification. The tool takes an architectural specification as input and generates a behavior protocol as output. The transformation rules are described independently from the transformation process. This allows changing the transformation rules without affecting the transformation process. We discuss in detail the transformation rules for transforming a trustworthy component-based system, formally specified in an architecture description language (TADL), to an extended timed automata specification. The goal is to formally verify trustworthiness properties claimed in the source model by model checking the trustworthiness properties in the target model. By varying the target model and the set of transformation rules the same tool can be used to obtain different target models and use different verification techniques.
UR - http://www.scopus.com/inward/record.url?scp=84884894147&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84884894147&partnerID=8YFLogxK
U2 - 10.1109/CSIT.2013.6588799
DO - 10.1109/CSIT.2013.6588799
M3 - Conference contribution
AN - SCOPUS:84884894147
SN - 9781467358255
T3 - 2013 5th International Conference on Computer Science and Information Technology, CSIT 2013 - Proceedings
SP - 326
EP - 333
BT - 2013 5th International Conference on Computer Science and Information Technology, CSIT 2013 - Proceedings
T2 - 2013 5th International Conference on Computer Science and Information Technology, CSIT 2013
Y2 - 27 March 2013 through 28 March 2013
ER -