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:
- Definição de uma metodologia de modelação formal a partir de documentos de requisitos.
- Definição de uma metodologia de modelação de arquitectura de sistemas.
- 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.
- 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.