Transforming architectural descriptions for formal analysis

Naseem Ibrahim, Mubarak Mohammad, Vangalur Alagar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication2013 5th International Conference on Computer Science and Information Technology, CSIT 2013 - Proceedings
Pages326-333
Number of pages8
DOIs
StatePublished - Oct 7 2013
Event2013 5th International Conference on Computer Science and Information Technology, CSIT 2013 - Amman, Jordan
Duration: Mar 27 2013Mar 28 2013

Publication series

Name2013 5th International Conference on Computer Science and Information Technology, CSIT 2013 - Proceedings

Other

Other2013 5th International Conference on Computer Science and Information Technology, CSIT 2013
CountryJordan
CityAmman
Period3/27/133/28/13

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Information Systems

Fingerprint Dive into the research topics of 'Transforming architectural descriptions for formal analysis'. Together they form a unique fingerprint.

Cite this