• Explicar as técnicas genéricas para análise de código de software. • Desenvolver ferramentas para analisar programas e sistemas de software. • Perceber o conceito de qualidade de software e modelos de qualidade de software. • Desenvolver analisadores de qualidadade de software baseado em métricas. • Construir ferramentas de software para a transformação, refactoring e evolução de programas. • Implementar algoritmos fundamentais de análise estática de programas
O programa consiste dos seguintes quatro áreas: • Análise de Código de Programas: Técnicas de Parsing Generalised e Scannerless, Combinadores de Parsing, Travessias Genéricas de árvores, Programação Estratégica, Análise de Tipos; Análise de fluxo de dados; Análise inter-procedimental; Análise de controlo de fluxo. • Qualidade de Software: Métricas para Código de Programas, Métricas para Sistemas de Software, Estudos Empiricos para analisar qualidade software, Modelos de qualidade de Software (CMMI, ISO 9126), Certificação de software. • Transformação de Software: Técnicas para Transformação e Refactoring de Programas (sistema TOM e RASCAL), Slicing e Cálculo Parcial de Programas,Técnicas para a Evolução de Software, Evolução em engenharia dirigida por modelos. • Teste de Software: Teste unitário e funcional; Análise da cobertura de teste; Teste orientado por modelos; Geração automática de cenários de teste; Injecção de falhas. Componente prática: JUnit + Emma, QuickCheck, PEX
O curso está organizado em duas componentes: um teórica onde são apresentados os conceitos teóricos e técnicas envolvidos nas quatro áreas estudadas na unidade curricular. Uma segunda componete prática será usada para os alunos desenvolverem um pequeno projecto ao longo do curso, onde os alunos terão oportunidade de utilizar ferramentas que usam os conceitos apresentados na parte teórica. A avaliação terá em conta estas duas componentes e com igual peso: na parte teórica será feito um teste individual escrito e na parte prática os alunos terão de desenvolver um projecto de software em grupo.
• Generative and Transformation Techniques in Software Engineering I, II, III, Ralf Laemmel, Joost Visser and João Saraiva editors, volumes 4143 and 5235 of LNCS Tutorials, proceedings of the summer schools GTTSE’05, GTTSE’07 and GTTSE’09, Springer. • Generative Programming - Methods, Tools, and Applications, Krzysztof Czarnecki and UlrichW. Eisenecker, Addison-Wesley, June 2000. • Partial Evaluation and Automatic Program Generation, N.D. Jones, C.K. Gomard, and P. Sestoft, Prentice Hall International, June 1993 • Domain Specific Languages, Martin Fowler, Addison-Wesley Professional, September, 2010 • Refactoring: Improving the Design of Existing Code, Martin Fowler, Kent Beck, John Brant,William Opdyke, Don Roberts, Addison Wesley, 2000. • Software Evolution, Tom Mens, Serge Demeyer, Springer 2008. • Software Testing, Ron Patton, Sams Publication 2006
Abstrair os detalhes de um componente de software por forma a obter um modelo adequado à verificação formal; Modelar o estado de um componente de software usando o conceito unificador de relação matemática; Especificar invariantes e pré- e pós-condições de operações usando lógica relacional; Especificar sistemas reactivos usando lógica temporal; Utilizar ferramentas de verificação automática para estabelecer a validade de uma propriedade de software.
Introdução: o papel dos métodos formais na engenharia de software; o papel da abstracção na modelação formal; lógica proposicional e de primeira ordem. Lógica relacional: sintaxe e semântica; modelação usando relações; introdução ao cálculo relacional; taxonomia e álgebra das relações. Alloy: especificação de invariantes e de operações usando pré- e pós-condições em lógica relacional; idiomas para modelação de comportamento dinâmico; semântica e sistema de tipos; técnicas para verificação automática; comparação com outras linguagens de modelação. Especificação de sistemas reactivos: lógica temporal (LTL e CTL); verificação de modelos por enumeração explícita do espaço de estados; verificação de modelos simbólica; ferramentas para verificaçao de modelos.
Metodologia de ensino: aulas teóricas expositivas; aulas teórico-práticas de demonstração de ferramentas e realização de exercícios. Avaliação: mini-projecto sobre Alloy (10%); mini-projecto sobre verificação de modelos (10%); exercício de leitura (10%); teste individual (70%). Os mini-projectos e exercício de leitura são realizados em grupos de 2 alunos.
Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
Esta Unidade Curricular, que é parte integrante do perfil em Métodos Formais em Engenharia de Software, tem por objectivo proporcionar formação em Arquitectura de Software numa perspectiva formal e com ênfase nos sistemas reactivos, nomeadamente introduzindo a. sistemas de transição como elementos arquitecturais de base b. fundamentos matemáticos correspondentes: álgebra relacional e linear c. paradigmas de modelação arquitectural: orientada aos processos e à coordenação d. técnicas de análise arquitectural ao nível estrutural, comportamental e de desempenho No final, o aluno deverá a. estar familiarizado com as noções básicas de arquitectura para sistemas reactivos b. ser capaz de modelar e analisar arquitecturas de software c. exibir competências práticas na utilização de ferramentas computacionais de suporte.
1. Introdução à arquitecture de software e aos sistemas reactivos: problemas, conceitos e métodos. 2. Fundamentos: 2.1 Sistemas de transição como elementos base em modelação de arquitectras para sistemas reactivos. Simulação, bissimulação e invariantes. Cálculo relacional e conexões de Galois. Relação com a lógica modal e as álgebras de processos. 2.2 Autómatos pesados e com evolução estocástica. Introdução à álgebra linear dos programas. 3. Paradigmas em modelação arquitectural 3.1 Orientação aos processos. Introdução a AADL. 3.2 Orientação à cooredanação. Introdução a Reo. 4. Análise arquitectural 4.1 Propriedades estruturais, comportamentais e desemepnho. 4.2 Cadeias de Markov interactivas - aplicação à análise arquitectural. Laboratório: Desenvolvimento de casos de estudo de média dimensão em modelação e análise arquitectural com recurso a ferramentas de suporte para AADL, Reo e cadeias de Markov.
O ensino é baseado em aulas teóricas e teórico-práticas, complementadas com sessões de demonstração e uso guiado de ferramentas A avaliação é por feita por teste individual escrito (60%) e pelo desenvolvimento de mini projectos com recuro às ferramentas estudas (40%).
A. Aldini, M. Bernardo, and F. Corradini. A Process Algebraic Approach to Software Architecture. Springer Verlag, 2010. F. Arbab. Reo: a channel–based coordination model for component composition. Mathematical Structures in Comp. Sci., 14(3):329–366, 2004. D. Garlan. Formal modeling and analysis of software architecture: Components, connectors and events. In M. Bernardo and P. Inverardi, editors, Third International Summer School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures (SFM 2003). Springer Lect. Notes Comp. Sci, Tutorial, 2004. Holger Hermanns. Interactive Markov Chains. Springer Verlag. 2002. J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series. American Mathematical Society, 2004.
• Explicar o funcionamento das técnicas mais importantes em verificação de software. • Especificar o comportamento de programas através de contratos. • Utilizar ferramentas para a verificação de programas anotados com contratos. • Explicar as diferentes abordagens que têm sido utilizadas para mitigar o problema de explosão do espaço de estados no model checking. • Utilizar uma ferramenta de model checking simbólico. • Utilizar ferramentas de verificação automática de software baseadas em model checking.
• Demonstração de Teoremas: introdução à construção interactiva de provas. • Teorias de Primeira Ordem: utilização de SMT solvers. • Verificação Dedutiva: lógicas de programas; geração de condições de verificação; linguagens de especificação comportamental de interfaces de código e design by contract. Componente prática: Dafny; Frama-C; SPARK. • Model Checking: model checking simbólico; redução de ordem parcial; bounded model checking. Componente prática: SMV. • Model Checking de Software: bounded model checking de código; mecanismos de abstracção existencial; abstracção baseada em predicados; refinamento de abstracções. Componente prática: CBMC; BLAST.
A escolaridade da UC é utilizada da seguinte forma - Duas horas téoricas (T) semanais são utilizadas para exposição da matéria e apresentação de casos de estudo. - Com uma vocação complementar às anteriores, duas horas semanais teórico-práticas (TP) para a resolução de exercícios e/ou apresentação de casos de estudo (com utilização das ferramentas estudadas) pelo docente; e possivelmente para outros pontos, como a discussão e acompanhamento de eventuais miniprojectos a desenvolver pelos alunos. A avaliação é feita através de dois testes, um intercalar e outro final, ambos com peso de 50%, ou alternativamente através de um teste (60%) e um miniprojecto de verificação, (40%).
- Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA. - Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press, Cambridge, MA, USA. - José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. 2011. Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer Publishing Company, Incorporated. - Aaron R. Bradley and Zohar Manna. 2010. The Calculus of Computation: Decision Procedures with Applications to Verification (1st ed.). Springer Publishing Company, Incorporated.