动态软件体系结构的正式框架：一个多学科的开放获取档案馆文件

动态软件体系结构的一个正式框架埃弗顿拉涅利·德索萨·卡瓦尔坎特引用此版本：埃弗顿拉涅利德索萨卡瓦尔坎特。动态软件体系结构的正式框架。软件工程[cs.SE]。University deBretagne Sud; Universidade federal do Rio Grande do Norte（Natal，Brésil），2016.英语NNT：2016LORIS 403. 电话：01426029HAL Id：tel-01426029https://theses.hal.science/tel-014260292017年1月4日提交HAL是一个多学科的开放获取档案馆，用于存放和传播科学研究文件，无论它们是否已这些文件可能来自法国或国外的教学和研究机构，或来自公共或私人研究中心。L’archive ouverte pluridisciplinaireUn framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016这些/南布列塔尼大学布列塔尼卢瓦尔大学校园为了获得南布列塔尼大学提及：STIC博士学校：SICMAPrésentée par埃弗顿Ranielly DE SOUSA CAVALCANTE6074混合研究单元准备Institut de Recherche en Informatique et Systemes AléatoiresUniversité Bretagne SudUn framework formelpour les architectureslogicielles dynamiquesThèse soutenue le 10 juin 2016，devant le jury composé de：M.保罗·罗伯托·弗雷雷·库尼亚Recife，Brésil，Pernambuco联邦大学校长M.哈利勒·德里拉法国国家科学研究中心研究主任/特别报告员Mme. Elisa Yumi NAKAGAWA巴西圣卡洛斯圣保罗大学人类发展报告会议主任/特别报告员M. Gibeon Soares AQUINO JUNIOR巴西纳塔尔北里奥格兰德联邦大学硕士/考试主任M. Jair Cavalcanti LeiteBrésil，Natal，北里奥格兰德联邦大学/考试主任M.卡洛斯·恩里克·库埃斯塔·金特罗西班牙马德里Rey Juan Carlos大学人类发展报告会议主任/考试主任Mme. Thais VASCONCELOS BATISTA巴西纳塔尔北里奥格兰德联邦大学人类发展报告会议主任/该司司长M.弗拉维奥·奥肯多Universités，IRISA - Université Bretagne Sud，Vannes，France / Directeur dethèseUn framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016动态软件体系结构埃弗顿拉涅利·德索萨·卡瓦尔坎特提交博士论文，部分符合计算机科学博士学位的要求，根据巴西北里奥格兰德联邦大学（UFRN）和法国南布列塔尼大学（UBS）之间的联合监督协议，担任信息学博士监事Thais Vasconcelos BatistaUniversidade Federal do Rio Grande do Norte，Natal，BrazilFlavio OquendoIRISA-UMR CNRS/Université Bretagne Sud，Vannes，France2016年6Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016致谢说没有任何事物是独自成长的：一个支持的眼神，一句鼓励的话语，一个理解的姿态，一种爱的态度总是必要的。也许很难用语言来表达，但我想对几个以某种方式直接或间接做出贡献的人说声这里仍然有可能引用其他人的话，但不幸的是，他们不是因为我的记忆出现了故障对那些人，我真诚而谦卑地道歉。我赞美上帝，生命的作者，因为他又给了我一次机会，也因为他在逆境中取得了成就我感谢他给了我毅力、力量和勇气去梦想，并为我的目标而奋斗，感谢他让我成为今天的我，感谢他让我把那些在我有限的眼睛看来遥远甚至不可能的事情具体化我感谢我的父母，玛丽亚·戈雷特和何塞·卡瓦尔坎特（在记忆中），感谢他们在困难中为我提供良好的教育所做的努力，感谢他们所坚持的原则和价值观，这些原则和价值观无疑是我将在余生中随身携带的元素他们教会了我如何有尊严和诚实地生活，让我看到道路超越你所能看到的从心底里，我感谢我的导师Thais Vasconcelos Batista教授（UFRN，巴西）和Flavio Oquendo教授（IRISA/Université Bretagne Sud，法国）所做的一切。生活是非常慷慨的，让我不仅与两位优秀的专业人士一起工作，而且与独特的人一起工作。总的来说，在博士期间的路线是非常困难的，但我可以说，这段时间对我来说是一个令人难以置信的快乐之旅毫无疑问，这是我们三人组的奉献精神、关注和伙伴关系的结果，直接反映在这项工作的质量他们总是让我自由，并提供成熟我的想法的手段，总是指出正确的方向。每走一步，我都更有信心，因为我知道我得到了他们的支持。即：对泰国人来说：我们生活中最大的愿望就是找到一个能让我们做到最好的人。我毫不怀疑，她是我学术生涯中最重要的人，到目前为止，我不知道还能从导师那里期待什么我绝对比我预期的要多，甚至是应得的，因为我有她的友谊，可用性，建议，耐心，信任，还有很多机会我非常感谢Thais的专业榜样，她每天都激励着我，主要是因为她是一个有着巨大心灵的人我在这里说的任何话都将是对她的由于这些和其他许多原因，这篇博士论文是献给她的。致弗拉维奥：我今天可以自豪地说，我是由世界上最...Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016著名的软件架构研究人员我非常感谢弗拉维奥，因为他积极回应了我的导师邀请，密切关注这项工作的进行，主要是在法国瓦纳张开双臂接待我，在那里度过了近两年的博士学位，距离我的家乡超过6000公里作为一名科学家，我已经成长了很多，这要归功于他的智慧，渊博的知识，承诺和远见，这是我将永远寻求遵循的标准我感谢教授Jair Cavalcanti Leite，Gibeon Aquino Junior（UFRN，巴西），PauloCunha （ UFPE ， 巴 西 ） ， Elisa Yumi Nakagawa （ USP ， 巴 西 ） ， Khalil Drira（Université Fédérale de Toulouse-Midi-Pyrénées，法国）和Carlos Cuesta（UniversidadRey Juan Carlos，西班牙），他们自愿抽出时间并接受邀请参加评估这篇博士论文的考试委员会这是一个伟大的荣誉，有优秀的研究人员愿意给他们的贡献，这项工作的数量。我感谢Flavia Coimbra Delicato和Paulo de Figueiredo Pires教授（UFRJ，巴西），他们参加了我的博士资格考试委员会这项工作的最后结果有他们的重要贡献，对此我非常感谢。我感谢那些或近或远的朋友，那些我几乎每天都能见到的朋友，那些我只能通过互联网“看到”的朋友遗憾的是，由于篇幅有限，而且有可能忘记某个人，或者说不公平，我无法一一列举所有人的名字，但请接受我在此表达的谢意。尽管如此，我还是想提到古斯塔沃·阿尔维斯和埃弗顿·利马，他们一直很亲密，可以与我分享一些时刻，并提供他们宝贵的友谊和支持，这是这次旅程的基本要素非常感谢我感谢来自IRISA/布列塔尼南大学的ArchWare集团Equipe de Recherche sur lesArchitectures Logicieles的研究人员特别要感谢Jean Quilbeuf，他直接参与并为这项工作做出了贡献，感谢他不断的可用性和耐心来解决我对软件架构中统计模型检查的疑问我感谢ICMC-USP（巴西圣卡洛斯）的同事和朋友，我在瓦纳时很高兴见到他们，并建立了富有成效的伙伴关系，特别是Lucas Oliveira，Milena Guessi和Elisa YumiNakagawa教授在这个团体中，我仍然需要向Marcelo Gonçalves表示感谢，不仅是因为我们在一起进行的几项工作中的伙伴关系，而且主要是因为他是一个特殊的人最后，我感谢那些鼓励实施这一项目并为这项工作的开展提供必要财政支持的机构：巴西国家石油、天然气和生物燃料局（ANP），通过石油和天然气地质学、地球物理学和信息技术人力资源方案（PRH-22）;巴西研究和项目供资局（FINEP）;巴西国家石油、天然气和生物燃料局（ANP），通过巴西国家石油、天然气和生物燃料局Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016科学、技术、创新和通信部（MCTIC）;巴西国家科学和技术发展委员会（CNPq）;以及巴西提高高等教育人员素质协调会（CAPES）。Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016阿格拉代森托斯Dizer的我们的信念和信念：永远正确地表达我们的支持，我们的激励，我们的祝福，我们的爱。Talvez seja difídizer isto em forma de palavras，mas gostaria de dizer这是一个非常重要的问题，因为它是一个非常重要的问题，因为它是一个非常重要的问题，因为它是一个非常重要的问题。这是我的真诚和谦卑。感谢上帝，感谢生命的作者，但这是一个让步的机会，也是一个征服我的机会。我非常高兴，因为我有毅力，有力量，有信心，有目标，有信心，有能力，有在我的国家，玛丽亚·戈雷特和何塞·卡瓦尔坎特（在纪念），我们必须克服各种困难，使我们的超通道与我们的通道相称，使我们的通道充满活力和价值，使我们的生活充满活力和价值。他让我活在尊严和诚实的生活中，让我相信他是正确的。Agradeço do fundo do coração aos meus orientadores ， os Professores ThaisVasconcelos Batista （ UFRN ， Brasil ） e Flavio Oquendo （ IRISA/Université BretagneSud，França），por absolutamente tudo.A vida foi muito generosa ao me permitir trabalharnão apenas com dois profissionais de excelência，mas sobretudo com seres humanos ípares.在杜托拉多重要的日子里，他们可能会说，他们的行为是为了让我感到幸福，因为他们有罪。如果你能做到这一点，那么你的工作和工作就不会是形式上的三重，而是直接反映出你的工作质量。他们总是允许我自由和适度地表达我的想法，表达我的想法，或者直接表达我的想法。你可以走过去，也可以相信你的话，也可以离开。名称：泰国人。我们最大的希望是让我们的生活与我们的外表相矛盾，或者让我们的阴部更美。我不认为这对我来说很重要，因为我不认为这对我来说很重要，但我希望我能成为一个东方人。我希望我的朋友们，我的朋友们。Thais sou muito grato pelo exemplo de profissional que me inspira a cada dia eprincipalmente pelo ser humano de coração pelo que elé.我想我们应该说的是，这是一个非常有意思的话题。杜托拉多的这一举动引起了人们的广泛关注.Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016弗拉维奥：我现在可以说，我非常了解这两个研究者的东方，但他们的软件架构是世界上没有的。Flavio非常高兴地告诉我，他对我的定位很有信心，他希 望我能 在那里工作，主要是为了我在瓦纳的工作，França，在Doutorado度过的这段时间里，他希望我能在我出生的土地上找到一个更好的地方。Cresci bastante como scientista e isso se deve muito ao seu exemplo desabedoria，profundo conhecimento，comprometimento e visão，um padrão quesempre procurarei seguir.Agradeço aos Professores Jair Cavalcanti Leite，Gibeon Aquino Junior（UFRN，Brasil），Paulo Cunha（UFPE，Brasil），Elisa Yumi Nakagawa（USP，Brasil），Khalil Drira（Université Fédérale de Toulouse-Midi-Pyrénées，França）e Carlos Cuesta（ Universidad Rey Juan Carlos ， Espanha ） que gentilmente disuseram do seu tempo eaceitaram o convicite para participarem do comitê examinador para avaliação desta tese deDoutorado.我希望我的这一天能让优秀的研究人员为我的工作做出贡献。Flavia Coimbra Delicato和Paulo de Figueiredo Pires教授（巴西UFRJ）的毕业生，他参加了Doutorado Minha Qualificação委员会的考试。最后的结果是，工作人员的贡献很大，而且他们的贡献也很大。我们是朋友和长期的朋友，我们每天都在看电视，我们随时都在看电视Infelizmente não vou poder citar o nome de todos，tanto pelo espaço disponível quanto pelorisco or injustiça de esquecer de alguém，mas recebam aqui as minhas palavras de gratido.同样，我们也要感谢古斯塔沃·阿尔维斯和埃弗顿·利马的名字，他们总是为我们而努力，我们的友谊和友谊是如此的珍贵，我们的友谊和友谊是如此的珍贵。Muito obrigado.ArchWareEm particularly ， agradecimentos especiais ao Jean Quilbeuf ， que teveparticipação e contribuição direta neste trabalho ， pela sua constante disponibilidade epaciência em sanar minhas dúvidas com relação a statistical model checking em arquiteturasde software.Agradeço aos colegas e amigos do ICMC-USP（São Carlos，Brasil），os quais tiveor prazer de conhecer no periíodo em que estive em Vannes e estabelecer profícuas parcerias，especialmente Lucas Oliveira，Milena Guessi e e Professora Elisa Yumi Nakagawa.这一组人表达了对马塞洛·贡萨尔维斯的感激之情，除了对年轻人的各种工作感兴趣外，他们的主要工作是特别的。Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016为此，我们建议设立一些机构，鼓励执行目的地项目，并为发展目的地工作提供 基 本 的 资 金 支 持 ： à Agência Nacional do Petroleo ， Gás Natural e Biocombustíveis（ANP），por meio do programma de Formação em Recursos Humanos em Geologia，Geofísica e Informática no Setor de Petroleo e Gás（PRH-22）; à Financiadora de Estudos eProjetos （ FINEP ） ; ao Ministério da Ciência ， Tecnologia ， Inovaçées e Comunicaçées（MCTIC）da República Federativa do Brasil; ao Conselho Nacional de DesenvolvimentoCientífico e Tecnológico （ CNPq ） ， e; à Coordenação de Pessoal de Nível Superior（CAPES）.Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016这项工作是在下列机构的资助下开展的：巴西国家石油、天然气和生物燃料署通过石油天然气地质、地球物理和信息技术人力资源方案（PRH-22）巴西研究和项目供资局巴西科学、技术、创新和通信部（MCTIC）巴西国家科学技术发展委员会（CNPq）巴西提高高等教育人员素质协调会（CAPES）Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016成功来自于完成目标的意志、决心和坚持即使没有达到目标，寻找和克服障碍的人至少会做出杰出的成就José de Alencar，巴西作家（1829-1877）一旦有疑问，我们就会下定决心，坚持到底。我不知道你有什么困难，我可不想让你当海军上将。José de Alencar，escritor brasileiro（1829-1877）Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016动态软件体系结构作者：Everton Ranielly de Sousa Cavalcante主管：Thais Vasconcelos Batista博士教授和Flavio OquendoABSTRACT软件体系结构在软件密集型系统的开发中起着重要的作用，以满足功能和非功能需求。特别是，动态软件体系结构已经出现，以解决当代系统的动态环境中运行，因此在运行时发生变化的特点。体系结构描述语言（ADL）用于表示软件体系结构，产生可以在设计时和/或运行时使用的模型。然而，大多数现有的ADL在几个方面具有局限性：（i）它们集中于架构的结构、拓扑方面;（ii）它们不提供用于表示架构的行为方面的足够支持;（iii）它们不允许描述关于架构的动态的高级方面;（iv）它们在自动验证体系结构属性和约束方面受到限制;（v）它们与实施层面脱节，从而导致体系结构和实施之间的不一致。为了解决这些问题，本文提出了形式化的动态软件体系结构框架。这一框架包括：（i）基于结构和行为观点描述软件体系结构的形式化语言-ADL;（ii）编程动态重构操作的规范;（iii）从体系结构描述自动生成源代码;（iv）基于统计模型检验（SMC）的方法来形式化地表达和验证动态软件体系结构中的属性。拟议框架的主要贡献有四个方面。首先，EST-ADL语言被赋予用于描述编程的动态重配置的体系结构级原语。第二，将EST-ADL中的架构描述转换为Go编程语言中的实现源代码，从而有助于最小化架构漂移。第三，一种新的逻辑，称为DynBLTL，用于形式化表达动态软件体系结构中的属性。第四，构建了一个依赖于SMC的工具链，以自动化架构属性的验证，同时努力减少执行此类任务的工作量、计算资源和时间。在这项工作中，两个无线传感器网络为基础的系统被用来验证框架元素。关键词：软件体系结构，体系结构描述语言，动态重构，形式验证，时序逻辑，统计模型检验。Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016Um Framework Formal paraArquiteturas de Software DinâmicasAutor：Everton Ranielly de SousaCavalcante Orientadores：Prof. Thais Vasconcelos Batista e Prof. Dr. FlavioOquendoRESUMO软件架构是一个重要的文件，没有开发软件系统的密集性，只允许满足一些功能需求。Emparticularly ， arquiteturasdesoftwaredinâmicastêmsurgidoparaendereçarcharacterísticas dos sistemas contemporâneos que operam em ambientes dinâmicos econsequentemente sujeitos a mudanças em tempo de execução.建筑语言描述（ADL）可用于软件建筑的代表，生产可用于项目执行速度的模型。然而，ADL存在的主要局限性在不同方面：(i) possui enfoque em aspectos estruturais，topológicos da arquitetura;（ii）não provêum supporte adequado à representação de aspectos comportamentais da arquitetura;（iii） não permite descrever aspectos avançados relativos à dinâmica da arquitetura;（iv）é limitada com relação à verificação de propriedades arquiteturais e restriçaçes，e;（v）é desconectada do nível de implementação，resultando em inconsistências entrearquitetura e implementação. No intuito de endereçar esses problemas ， esta tesepropioneeumframeworkformalparaarquiteturasdesoftwaredinâmicas.Talframeworkenvolve ： （ i ） EAS-ADL ， uma linguagem formal para descreverarquiteturas desoftware sob as perspectivas estructural e comportamental; （ ii ） aspecificação de operaçeses de reconfiguração dinâmada;（iii）a geração automática decódigo fonte a partir de descreçeses arquiteturais，e;（iv）uma abordagem basada emverificação estatística（SMC）para expressar e verificar formalmente propriedades emarquiteturas desoftware dinâmada.As principais contribuiçais trazidas pelo frameworkproposto so quatro. Primeiro，a linguagem pastou a ser dotada de acquitivas de nvelarquitetural para decrever reconfigurasdinâmicas madas. 第二部分，描述了建筑学中的ADLsão traduzidas para código fonte de implementação na linguagem de PummaçãoGo，contributindo assim para minimizar desvios arquiteturais。第三，一个新的lógicachamadaDynBLTLéutilizadaparaexpressarformalmentepropriedadesemarquiteturas desoftware dinâmicas. Quarto ，um ferramental basado em SMC foi juídopara automatizar verificação de propriedades arquiteturais enquanto busca reduziresforço，recursos computacionais e tempo para realizar essa tarefa. Neste trabalho，doissistemas basedos em redes de sensores sem fio são utilizados para validar os elementosdoframework.Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016Palavras-chave：Arquiteturas de software，Linguagens de descrição arquitetural，Reconfiguração dinâmica，Verificação formal，Lógica temporal，Verificação estatística.Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016联合国动态逻辑架构框架Auteur：Everton Ranielly de SousaCavalcante导演：Dr Thais Vasconcelos Batista（MCF-HDR）and Pr Flavio OquendoRESUME逻辑架构在系统发展中发挥着重要作用，主要是为了满足功能需求和功能外需求。特别是，动态逻辑架构应融合于动态系统中运行的当代系统的特性，并在执行过程中进行相应的变更。建筑描述语言（ADL）是用来表达建筑逻辑的语言，它可以用来表达建筑的概念，也可以用来表达建筑的执行。然而，ADLs的大部分存在并不局限于多个方面：（i）它不描述建筑的结构、拓扑方面;（ii）它不知道如何支持建筑的构成方面;（iii）它不允许描述建筑的动态方面;（iv）它不局限于建筑产权和建筑约束的自动更新; et（v）ils sontdconnects du niveau d'implmentation et entraavernent souvent des incohcilientrel'architecture et l'implmentation.面对这些问题，本文提出了一个动态逻辑体系结构框架。Ce骨架化合物：（i）E-ADL，un langage formel pour dcrire des architectureslogicieles dynamiques sous les perspectives structurelles et comportementales ;（ii）laspeccification des oprations de reconfiguration dynamique programme ; （ iii ） lagnration automatique de code source  partir des descriptions architecturales ;和（四）一种基于统计验证的方法，以探索和验证动态逻辑结构的所有权。拟议框架中的主要贡献是四个方面。首先，le langage Z-ADL a t dot de primitives de niveau architecturalpour dcrire des reconfigurations dynamiques programmes.第二，在编程语言Go中，对体系结构的描述与实现代码源的转换，有助于最小化体系结构的描述。第三，一个新的逻辑称为DynBLTL est utilise exprimer formellement des proprits dans les architectureslogicielles dynamiques 。 Quatrimement ， un outil bas sur SMC a t dcamp pourautomatiser la vrification des proprits architecturales en cherchant  rduirel'effort，les resources computationnelles，et le temps pour réaliser cette tâche. 在工作中，两个系统Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016basés sur réseaux de capacitors fil sont utilisés pour valider les eléments du framework.格言：逻辑架构、架构描述语言、动态重构、形式验证、时序逻辑、统计验证。Un framework formel pour les architectures logicieles dynamiques Everton Ranielly De Sousa Cavalcante 2016图目录图1.............................................................................................................................................图2.............................................................................................................................................图3 -..........................................................................................................................................图4.............................................................................................................................................图5.............................................................................................................................................图6.............................................................................................................................................图7-...........................................................................................................................................图8--..........................................................................................................................................图9-图10...........................................................................................................................................图11-简单客户机-服务器架构的动态重新配置的外生方法的说明。在主服务器不可用的情况下，主服务器由辅助服务器替换...................................................