EVOLVE

Definição de métodos formais para especificações e arquitectura

Esta tarefa propõe a introdução de métodos formais na definição e modelação de requisitos e arquitectura. Esses métodos deverão também contribuir para a definição de regras e standards que ajudem a captar eficazmente propriedades inerentes aos requisitos (arquitectura) que possam ser validados e verificados formalmente de forma (semi) automática.

As etapas desta tarefa são as seguintes:

1. Definição de uma metodologia de modelação formal a partir de documentos de requisitos.
2. Definição de uma metodologia de modelação de arquitectura de sistemas.
3. Análise de um caso de estudo com vista ao 'fine tuning' das metodologias (1)+(2) a problemas do domínio de aplicação do projecto.
4. Estudo da semântica do SysML com vista à sua futura adopção nas metodologias propostas

À partida, propõe-se a abordagem que é adoptada na U.Minho e que se centra na filosofia "model-based" na generalidade e "state based" em particular, o que cobre praticamente todos os métodos em uso nos dias de hoje. Essa abordagem tem por base a combinação de ferramentas de modelação formal e prototipagem rápida com as de model-checking. Em concreto, propõe-se a utilização do standard VDM-SL (ISO/IEC 13817-1) e das suas extensões VDM++ e VICE (esta para tempo real) que se articulam com UML em regime de round-trip engineering. O pacote de ferramentas VDMTools (CSK, Japão, com quem a U.Minho tem um acordo de investigação) contempla o standard ISO bem como as referidas extensões, gerando ainda obrigações de prova de correcção (proof obligations) que podem ser validadas recorrendo a model-based testing ou passadas ao model checker para geração de contra-exemplos. Aqui propõe-se o Alloy Analyzer 4.0 RC11, cuja eficácia na detecção de fraquezas de modelos é bem conhecida. O uso de OCL como alternativa ou complemento a VDM deve também ser considerado, já que a distância entre as duas linguagens não é muita (OCL baseia-se em associações e especificação de operações via pares pre/post-condição), ainda que OCL tenha uma semântica mais imprecisa.