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

  1. 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.
  2. Experimental Prover back-end for TLA+. Again this could be done in different ways, such as translating TLA+ to HLL.
  3. Experimental translation of Hybrid automata to HLL, see "Symbolic Simulation of Dataflow Synchronous Programs with Timers" by Guillaume Baudart, Timothy Bourke, and Marc Pouzet.
  4. Experimental translation of Solidity (Ethereum's language for writing smart contracts) to HLL.
  5. 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):

  1. 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