Describing correct deployment architectures based on a bigraphical multi-scale modeling approach. (October 2017)

• Record Type: Journal Article
• Authors: Gassara, Amal; Bouassida Rodriguez, Ismael
• Is Part Of: Computers & electrical engineering. Volume 63(2017)
• Page Start: 277
• Page End: 288
• Publication Date: 2017-10
• Subjects: Deployment architectures -- Formal methods -- Bigraphs -- Multi-scale modeling -- Correct by design; Computer engineering -- Periodicals; Electrical engineering -- Periodicals; Electrical engineering -- Data processing -- Periodicals; Ordinateurs -- Conception et construction -- Périodiques; Électrotechnique -- Périodiques; Électrotechnique -- Informatique -- Périodiques; Computer engineering; Electrical engineering; Electrical engineering -- Data processing; Periodicals; Electronic journals; 621.302854
• DOI: 10.1016/j.compeleceng.2017.05.018
• Languages: English
• ISSNs: 0045-7906

Abstract

Highlights: A formal approach for describing deployment architectures and their reconfigurations. A multi-scale modeling approach using Bigraphical Reactive Systems. Correct by design deployment architectures. An illustration of our approach with a Smart Home case study. Graphical abstract: Abstract: In this paper, we propose a formal approach supporting the correct description of deployment architectures and their reconfigurations. According to defined models, correct deployment architectures are generated and one of them is selected to be deployed. This generation process is based on a multi-scale modeling approach adopting Bigraphs and Bigraphical Reactive Systems as a modeling language. In fact, the architecture of a scale is refined by adding the components of the next scale. Then, the obtained architecture is in turn refined and so on, until reaching the last scale. The transition between scales is performed through applying refinement rules. Based on correct by design, the refinement process is executed on a correct scale architecture (respects the defined models) by applying correct rules. So, we ensure that the generated scale architectures are correct. Finally, our approach is illustrated through the case study Smart Home.