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 |
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:
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)