Cohesive Project (Lab. EI)
Material
Interesting and useful slides for preparing your milestone presentations:
Projects
Project ideas from
Prover Technology (if you are interested in any of these projects please contact Alcino Cunha):
- Experimental Prover back-end for Alloy or (preferably) Electrum. This could be done in several ways. One way would be to translate Alloy/Electrum models into HLL models. Another (probably simpler) way would be to translate some internal representation used by Alloy/Electrum directly to LLL.
- Experimental Prover back-end for TLA+. Again this could be done in different ways, such as translating TLA+ to HLL.
- Experimental translation of Hybrid automata to HLL, see "Symbolic Simulation of Dataflow Synchronous Programs with Timers" by Guillaume Baudart, Timothy Bourke, and Marc Pouzet.
- Experimental translation of Solidity (Ethereum's language for writing smart contracts) to HLL.
- Take any modeling/verification problem that you could have reasonably approached using Alloy or TLA+, model it in HLL and verify it using PSL. This case study would be particularly interesting, since it has already been approached using Electrum (see Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum).
Glossary:
- HLL: Prover's high-level language for modeling reactive systems (predicate logic and rich data types).
- LLL: Prover's low-level language for modeling reactive systems (propositional logic).
- PSL: Prover's model checker.
Project proposed by J.C. Ramalho (contact person: J.N. Oliveira):
- Formal modelling of a support system for a TS-RADA ontology for the M-51-CLAV platform.
Students
| # | Nome | Curso |
|---|
| a82441 | Alexandre Mendonça Pinho | MIEI |
| a80453 | Bárbara Andreia Cardoso Ferreira | MIEI |
| pg40866 | Bruno Manuel Pereira Antunes | MMC |
| a80564 | Carla Isabel Novais da Cruz | MIEI |
| a83344 | Eduardo Jorge Lima Pinto Barbosa | MIEI |
| a78073 | João Costeira Faria Gomes | MIEI |
| a80397 | João Nuno Alves Lopes | MIEI |
| a82885 | José Augusto Ferreira Alves | MIEI |
| a68547 | Lucas Ribeiro Pereira | MIEI |
| a74036 | Manuel João Curopos Monteiro | MIEI |
| a82400 | Márcio Alexandre Mota Sousa | MIEI |
| a82535 | Pedro Mendes Pinto | MIEI |
| pg41094 | Pedro Rafael Paiva Moura | MEI |
| a82313 | Pedro Teixeira Gonçalves | MIEI |
| a75411 | Ricardo Guerra Leal | MIEI |
| a73577 | Ricardo Ribeiro Pereira | MIEI |
| a82572 | Sara Maria Barreira Melo | MIEI |
| a75328 | Tiago João Fernandes Baptista | MIEI |
--
JoseNunoOliveira - 13 Jan 2020
2020/21.
30 Mar - VF: alteração do método de avaliação. 
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.