Arquitectura e Cálculo

Índice

Objectivos

Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos.

Resultados de aprendizagem

• *Conhecer e caracterizar modelos para computação reactiva baseados em diferentes tipos de sistemas de transição, nomeadamente com evolução não-determinística, em tempo real ou estocástica.
• *Formular propriedades sobre esses modelos e analisar a sua satisfação.
• *Familiarizar-se com a noção de coordenação de software e utilizá-la produtivamente na definição de arquitecturas de sistemas reactivos.
• *Conhecer e utilizar ferramentas computacionais de suporte.
• *Integrar os conhecimentos adquiridos para utilização no projecto de engenharia de sistemas reactivos.

Programa Resumido

• Introdução aos sistemas reactivos
• Fundamentos
  • Semântica: Sistema de transição etiquetado. Morfismo. Noção de simulação e bissimulação. Bissimilaridade e sua relação com noções intuitivas de equivalência de comportamentos.Composição concorrente de sistemas de transição.
  • Lógicas: Introdução às lógicas modais e temporais. Taxonomia de propriedades dos sistemas reactivos. Tempo linear e tempo ramificado. Nominais e lógica híbrida.
• Modelação e análise de sistemas reactivos
  • Sistemas de transição não determinísticos (mCRL2).
  • Sistemas com requisitos de tempo real (Uppaal).
  • Sistemas com evolução probabilística (IMC).
• Arquitectura de sistemas reactivos
  • Motivação: Arquitectura de sistemas reactivos.
  • O paradigma de coordenação: Interacção mediada por conectores.
  • O modelo e a linguagem reo: Sintaxe e semântica. *Projecto e integração de ferramentas.

Material de Apoio (notas e slides)

Software Architecture for Reactive Systems

Background: Labelled Transition Systems

Background: Modal, Temporal, Hybrid Logics

Time-critical Systems

Probabilistic Systems

Architectural design: the coordination perspective

Coordination and Software Composition (Invited Lecture by Prof Farhad Arbab)

Bibliografia recomendada

• J. Groote e M. Mousavi: Modeling and analysis of communicating systems. MIT Press, 2014.
• L. Aceto et al: Reactive systems: Modelling, specification and verification. Cambridge University Press, 2007.
• H. Hermanns: Interactive Markov chains: The quest for quantified quality. Springer Lect. Notes Comp. Sci. (2428), 2002.

Bibliografia complementar

• C. Baier e J.-P. Katoen: Principles of Model Checking. MIT Press, 2008
• P. Blackburn, M. Rijke e Y. Venema: Modal Logic. Cambridge University Press, Cambridge, 2001.
• T. Brauner: Hybrid Logic and its Proof-Theory. Applied Logic Series, Springer, 2010.
• A. Aldini, M. Bernardo e A. Corradini: A Process Algebraic Approach to Software Architecture. Springer Verlag, 2010.

Ferramentas

Funcionamento

Docente

• Luís Soares Barbosa

Avaliação

• Prova individual escrita (70%)
• Mini-projecto de grupo (30%)
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

• Aviso: exame de recurso é dia 17 --- Todos os alunos, qualquer que tenha sido a nota obtida no teste, poderão comparecer.
• Aviso: dia 17 é também a deadline para a entrega de todos os trabalhos

• As classificações FINAIS encontram-se aqui.

Atendimento

-- Luís Soares Barbosa - 18 Julho 2015, 16.00h

13 Jul - Milestone 3 de LEI: está marcada para quarta-feira, 15 de Julho, das 9h00-13h00, na sala DI 1.08. Ver o escalonamento das apresentações no Calendário.

01 Jun - Milestone 2 de LEI: está marcada para quarta-feira, 17 de Junho, às 9h, na sala DI 1.08.

11 Abr - Milestone 1 de LEI: está marcada para quarta-feira, 15 de Abril, às 9h, na sala DI 1.08.

03 Mar - Publicada na página do Laboratório EI a alocação dos grupos aos projectos.

22 Fev - A "Workshop 0" de arranque dos projectos de MFES terá lugar na sala Di 1.08 no dia 25-Fev, ver Calendário.

Equipa docente

Luís Soares Barbosa
Manuel Alcino Cunha
Maria João Frade
José Nuno Oliveira
Joost Visser (docente convidado - SIG)

Verificação Formal

Docente: Maria João Frade

Slides

• Apresentação
• Propositional Logic and SAT solvers
• First-Order Logic and SMT
• SMT solvers
• Semantics: slides1, slides2, slides3, slides4
• Deductive Program Verification
• Deductive Program Verification with Frama-C: part1, part2
• Bounded Model Checking of SW: Introduction to CBMC, CBMC by Example
• Logic and Type Theory
• The Coq Proof Assistant: part1, part2, part3

Exemplos

• SAT
  • The unicorn puzzle

• SMT
  • Scheduling problem
  • Modeling assignments and array updates

• Frama-C
  • Ficheiros para as aulas
  • Alguma documentação

• CBMC
  • Ficheiros para as aulas
  • Alguma documentação

• Coq
  • Ficheiros para as aulas
  • Alguma documentação
  • Ficha de exercícios

Ferramentas

• SATLIB - The Satisfiability Library
• SMT-LIB - The Satisfiability Modulo Theories Library
• Frama-C - Software Analyzers
• CBMC - A Bounded Model Checker for C and C++ programs.
• The Coq Proof Assistant

• Máquina virtual com todas as ferramentas instaladas: Xubuntu-64bit.ova README

Provas de Avaliação

• Enunciado do projecto (SMT solvers) (Entrega: 26 de Abril) -- Notas
• Avaliação laboratorial sobre Frama-C e CBMC: 7 de Maio. -- Notas
• Avaliação laboratorial sobre Coq: 18 Junho. -- Notas

Notas Finais

• Época Normal
• Recurso

50 Recent Changes in TWiki Web retrieved at 17:22 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Bem vindo a MFES

Bem vindo à página da edição de 2013/14 da UCE de Métodos Formais em Engenharia de Software. O meu nome é José Nuno Oliveira e sou o responsável por este perfil de especialização do MEI, que conta com uma equipa de docentes altamente qualificados na investigação e ensino de métodos formais aplicados ao desenvolvimento de software. Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais desde há mais de 25 anos.

Nos seus 30 ECTS de ensino em métodos científicos de programação, incluindo 10 ECTS de acompanhamento de projectos propostos por parceiros industriais nacionais e estrangeiros, este perfil é porventura um dos mais expressivos na sua área.

As disciplinas que compoem MFES corporizam os principais vectores de que depende o projecto de aplicações fiáveis, à escala industrial. Na sua componente teórica, a visão é a de abordar problemas de software segundo uma autêntica perspectiva de engenharia, que permite - através da modelos matemáticos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos.

Na sua componente prática, a UCE ensina a conceber e animar modelos de problemas, testando-os atempada e exaustivamente antes de se proceder à fase de cálculo e implementação, por forma a evitar erros de perspectiva ou infantilidades de concepção. Em suma: ensina-se a saber modelar e calcular, sim, mas também a saber analisar, testar e avaliar, sem descurar métricas para a qualidade do software.

No seu conjunto, os conteúdos desta UCE pretendem realizar o desígnio de que é possível afixar o carimbo

nos artefactos de software desenvolvidos segundo os seus princípios metodológicos.

Parcerias

Classificação ACM

Número de ECTS por área de conhecimento, segundo as IEEE/ACM Curriculum Guidelines for Software Engineering:

• Software/SOFTWARE ENGINEERING/Metrics --- 2
• Software/SOFTWARE ENGINEERING/Requirements/Specifications --- 6
• Software/SOFTWARE ENGINEERING/Software Architectures --- 6
• Software/SOFTWARE ENGINEERING/Software/Program Verification --- 6
• Software/SOFTWARE ENGINEERING/Testing and Debugging --- 4
• Theory of Computation/LOGICS AND MEANINGS OF PROGRAMS/Specifying and Verifying and Reasoning about Programs --- 6

Citações

Humor

(Source: Software Development: A Rigorous Approach by C.B. Jones)

Education/MFES1415 Web Preferences

The following settings are web preferences of the Education.MFES1415 web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Preferences Settings

These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.

Natural Skin configuration

• Set SKIN=nat

• Set SKINSTYLE = Plain
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE = Métodos Formais em Engenharia de Software

• Set NATWEBLOGO = Métodos Formais em Engenharia de Software

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the Education/MFES1415 web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.

• Set WEBLOGOURL = WebHome
• Set #WEBLOGOIMG =
• Set WEBLOGOIMG =
• Set WEBLOGOALT = Métodos Formais em Engenharia de Software

• List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/MFES1415.Topic links.
  Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
  
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = Métodos Formais em Engenharia de Software
  • Set SITEMAPUSETO = Mestrado de [Engenharia] Informática (14/15)
  • Note: Above settings are automatically configured when you create a web

• Exclude web from a web="all" search: (Set to on for hidden webs).
  • Set NOSEARCHALL =
  • Note: This setting is automatically configured when you create a web

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Education/MFES1415 web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • Set ALLOWWEBCHANGE = AlcinoCunha, LuisSoaresBarbosa, JoseNunoOliveira, JorgeSousaPinto, MariaJoaoFrade
  • #Set DENYWEBRENAME =
  • Set ALLOWWEBRENAME = AlcinoCunha, LuisSoaresBarbosa, JoseNunoOliveira, JorgeSousaPinto, MariaJoaoFrade

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Tópicos

• Benvindo a MFES
• Sumários
• Análise e Teste de Software
• Especificação e Modelação
• Arquitectura e Cálculo
• Verificação Formal
• Lab. de EI
• Página principal
• Docentes

• MFES Alumni

Avisos

Create New Topic in Education/MFES1415 Web

Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.