Detalhes
Nome
Nuno Moreira MacedoCluster
InformáticaCargo
Investigador SéniorDesde
01 novembro 2011
Nacionalidade
PortugalCentro
Laboratório de Software ConfiávelContactos
+351253604440
nuno.m.macedo@inesctec.pt
2020
Autores
Cunha, A; Macedo, N;
Publicação
International Journal on Software Tools for Technology Transfer
Abstract
This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification. © 2019, Springer-Verlag GmbH Germany, part of Springer Nature.
2020
Autores
Cunha, A; Macedo, N; Liu, C;
Publicação
Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings
Abstract
2020
Autores
Macedo, N; Cunha, A; Pereira, J; Carvalho, R; Silva, R; Paiva, ACR; Ramalho, MS; Silva, DC;
Publicação
Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings
Abstract
2020
Autores
Liu, C; Macedo, N; Cunha, A;
Publicação
Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings
Abstract
2019
Autores
Santos, A; Cunha, A; Macedo, N;
Publicação
Proceedings - 3rd IEEE International Conference on Robotic Computing, IRC 2019
Abstract
The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system's architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before. © 2019 IEEE.
Teses supervisionadas
2019
Autor
André Filipe Faria dos Santos
Instituição
UP-FCUP
2019
Autor
Gonçalo Nuno Esteves Duarte
Instituição
UM
2019
Autor
Chong Liu
Instituição
UP-FCUP
2018
Autor
André Filipe Faria dos Santos
Instituição
UM
2016
Autor
Eduardo Jose Dias Pessoa
Instituição
UM
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.