Modelos de Sistemas de Software

Conhecimentos de Base Recomendados

Matemática discreta, incluindo lógica de predicados, conjuntos, funções, relações e técnicas de prova (tais como indução).

Métodos de Ensino

Esta unidade curricular inclui aulas teóricas de exposição detalhada de conceitos, princípios e técnicas fundamentais de modelação formal, em paralelo com exemplos práticos para estimular o interesse dos alunos pelos conceitos teóricos e exemplificar a sua aplicação a situações reais. Para dar mais tempo para responder a questões detalhadas há aulas semanais de natureza prática e de discussão. Estas sessões têm como objetivo olhar de perto para os trabalhos de casa semanais e para os projetos. Os alunos têm leituras semanais, com exercícios para resolver em casa, e três projetos em grupo.

Resultados de Aprendizagem

Os fundamentos científicos da Engenharia de Software dependem do uso de modelos abstratos e lógicas com elevada precisão, por forma a caracterizar e raciocinar sobre propriedades de sistemas de software. Existem diversos modelos básicos e lógicas que, ao longo do tempo, provaram ser particularmente importantes e ubíquas no estudo de sistemas de software. Esta unidade curricular foca esse corpo de conhecimento.

Após a conclusão desta disciplina, os alunos conseguirão (i) compreender as forças e fraquezas de certos modelos e lógicas, incluindo máquinas de estados, modelos algébricos e de processos, e lógica temporal, (ii) selecionar e descrever modelos abstratos apropriados para diversas classes de sistemas, descrever relações de abstração entre diferentes níveis de descrição, e raciocinar acerca da correção de refinamentos, e (iii) provar propriedades elementares de sistemas modelados através de técnicas introduzidas pela unidade curricular.

Estágio(s)

Não

Programa

- Introdução: informação sobre a disciplina; o que um modelo é.

- Fundamentos: lógica; técnicas de prova; sequências; conjuntos, relações e funções.

- Sistemas de eventos discretos; máquinas de estados finitos; raciocínio sobre máquinas de estados.

- Introdução à verificação de modelos; verificação de programas sequenciais.

- Concorrência; máquinas de estados concorrentes; técnicas de modelação; raciocínio sobre concorrência.

- Lógica Temporal Linear; propriedades de segurança e vivacidade; raciocínio automático e verificação formal.

- Modelação de sistemas distribuídos; raciocínio sobre processos comunicantes.

- Métodos formais no mundo real.

Docente(s) responsável(eis)

Raul André Brajczewski Barbosa

Métodos de Avaliação

Avaliação
Exame: 30.0%
Projecto: 70.0%

Bibliografia

Livros essenciais | Required textbooks:

- Introduction to Discrete Event Systems, C. G. Cassandras et al., Springer, 2008.

- Principles of the Spin Model Checker, M. Ben-Ari, Springer, 2008.

Opcional | Optional:

- Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth et al., Cambridge, 2004.

- Concurrency: State Models and Java Programs, J. Magee et al., 2nd Ed., Wiley, 2006.

- The Spin Model Checker: Primer and Reference Manual, G. J. Holzmann, Addison-Wesley, 2004.

- Verificação de Modelos, R. Barbosa, 2018.

Suplementar | Supplemental:

- Concepts and Notations for Concurrent Programming, G. R. Andrews et al., Computing Surveys, Vol. 15, No. 1, 1983.

- Formal Methods: State of the Art and Future Directions, E. M. Clarke et al., ACM Computing Surveys, Vol. 28, No. 4, 1996.

- A Primer on Model Checking, M. Ben-Ari, ACM Inroads, Vol. 1, No. 1, 2010.

- The Model Checker Spin, G. J. Holzmann, IEEE Transaction on Software Engineering, Vol. 23, No. 5, 1997.