MDA-Veritas: uma arquitetura MDA estendida para transformações de sistemas concorrentes preservadoras de semântica. - BARBOSA, Paulo Eduardo e Silva. (2011)
MDA é uma tendência de desenvolvimento de software que visa alterar o foco e os esforços dos modelos de desenvolvimento atuais. O método de implementação deixa de ser apenas a produção e código, e passa a também envolver modelos, metamodelos e transformações. Atualmente, essa abordagem tem sido diversiﬁcada com a inclusão de novos paradigmas que vão bem além do uso exclusivo dos padrões da OMG, como proposto originalmente. Contudo, a arquitetura MDA ainda sofre com a falta de formalização de alguns de seus artefatos e processos, levando a vários tipos de questionamentos. Um exemplo pertinente de questionamento se dá sobre o alto grau de ambigüidade dos modelos e transformações, originando problemas de baixa conﬁabilidade. Uma das conseqüências disso é o fato de que atualmente não existe uma maneira de garantir que transformações MDA sejam preservadoras de semântica, e nem que seus modelos envolvidos nas transformações sejam formais o suﬁciente para se permitir o uso de técnicas deveriﬁcação de equivalência, gerando críticas sobre a eﬁcácia dessa abordagem. Esta tese de doutorado propõe lidar com esse problema, incorporando abordagens consolidadas de métodos formais na arquitetura MDA, tendo como contexto especíﬁco o desenvolvimento de software para sistemas embarcados com características de concorrência. Propomos extensões para parte da arquitetura MDA para que se possa construir modelos semânticos que representem aspectos estáticos e dinâmicos, ambos essenciais na semântica dos modelos envolvidos nas transformações e nos mecanismos de veriﬁcação de equivalência desses modelos. Com isso,obtemos a veriﬁcação de equivalência em transformações envolvendo modelos de sistemas concorrentes. Como avaliação do trabalho, provas de conceito, estudos de caso e avaliação experimental seguindo a abordagem GQM, envolvendo parcerias na academia e na indústria através de sistemas reais, foram implementados e avaliados. Veriﬁcamos equivalência entre modelos ao nível de transformações PIM-para-PIM, PSM-para-PSM e PIMpara-PSM como modelos de sistemas concorrentes descritos em redes de Petri e algumas de suas extensões.