MFP

Logo

Índice

Métodos Formais em Engenharia de Software
Cálculo de Sistemas de Informação
Programação Ciber-física
Verificação Formal
Calendário | Sumários
Anos anteriores
Alumni

CSI/2023-24

CSI/2023-24/Método B

Grupos

Nome # Método Grupo Tema
Rui Pedro Esteves Vasques Correia de Oliveira PG54210 B G01 BPMN
Tiago Miguel Moreira Bacelar Pereira PG54257 B G01 BPMN
João Afonso Alvim Oliveira Dias de Almeida pg53902 B G01 BPMN
Jéssica Macedo Fernandes a93318 B G02 RDF
Vitor Lelis Noronha Leite pg54273 B G02 RDF
João Pedro Rodrigues Carvalho pg50496 B G02 RDF

Os grupos devem:


Temas

A) RDF

RDF (acrónimo de “Resource Description Framework”) é um modelo para publicação e troca de dados no Web padronizado pelo W3C. É baseado em triplos que registam relacionamentos entre objectos, formando o que se costuma chamar uma triple-store. Por esse motivo, a informação assume o formato de um enorme grafo, ou rede semântica. O modelo triple-store tem cada vez mais aceitação por ser bastante flexível e capaz de lidar com consultas semânticas poderosas, usando inferência para descobrir nova informação a partir de relacionamentos existentes.

Sendo óbvia a ligação entre RDF e a álgebra relacional (fortemente) tipada estudada nesta UC*, pretende-se neste projeto fazer uma formalização do primeiro na segunda, tirando partido das suas bases teóricas sólidas. Por exemplo, como se garante em RDF que um relacionamento é injectivo, simples, etc? Como se formulam e garantem invariantes?

Sugere-se o recurso ao Alloy Analyser para validar a formalização a fazer, sem prejuízo de se poderem usar outras ferramentas que se considerem adequadas.

Referência: A Formal Graph Model for RDF and Its Implementation por Vinh Nguyen, Jyoti Leeka, Olivier Bodenreider Amit Sheth (2016).

B) BPMN

A sociedade civil está organizada em torno do serviços de cuja eficácia e rigor todos dependemos. Esses serviços organizam-se por sua vez em processos, que se pretendem confiáveis. BPMN é um standard OMG para definição de processos oferecido como uma notação que, aberta e gráfica, é serializável em XML. Existem ferramentas (por exemplo Camunda) que a implementam, oferecendo interfaces gráficas intuitivas e fáceis de usar.

Tomando como ponto de partida a referência dada abaixo, pertende-se neste projeto formalizar o essencial da notação BPMN em álgebra relacional. Sugere-se o recurso ao Alloy Analyser para validar essa formalização, sem prejuízo de se poderem usar outras ferramentas que se considerem adequadas.

Referência: Formal Semantics and Automated Analysis of BPMN Process Models por Remco Dijkman, Marlon Dumas, Chun Ouyang (2007)