Cálculo de Programas

Licenciatura em Engenharia Informática
View   r30  >  r29  >  r28  >  r27  >  r26  ...

WebHome 30 - 22 Feb 2011 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2010/11 da disciplina de Cálculo de Programas.

Line: 28 to 28
 
Pedro Nunes(1502-1578) in Libro de Algebra, 1567, fol 270r.
Changed:
<
<
  • Análise de programas: escrever programas funcionais com recurso a combinadores algébricos.
>
>
  • Construção de programas: escrever programas funcionais de forma composicional, com recurso a combinadores algébricos.
 
Changed:
<
<
  • Transformação de programas: recurso à algebra da programação para se obterem programas mais eficientes a partir de outros.
>
>
  • Transformação de programas: recurso à algebra da programação para se obterem programas mais eficientes sem comprometer as sua correcção.
 
Changed:
<
<
  • Compreensão de programas: recurso à factorização em pares "fold" + "unfold" (hilomorfismos) como forma de se perceber o significado de um programa funcional.
>
>
  • Análise e compreensão de programas: recurso à factorização em pares "fold" + "unfold" (hilomorfismos) como forma de se perceber a arquitectura dos algoritmos e sua catalogação.
 
  • Síntese de programas: cálculo de ciclos-for a partir de definições indutivas da matemática.

WebHome 29 - 15 Feb 2011 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2010/11 da disciplina de Cálculo de Programas.

Line: 10 to 10
 A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.
Changed:
<
<
Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros subtis que os testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.
>
>
<-- Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros subtis que os testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem. !-->
 
Changed:
<
<
Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.
>
>
Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma reflectida, capaz de evitar erros de programação. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.
 A Universidade do Minho tem uma longa tradição neste tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de

WebHome 28 - 15 Feb 2011 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Changed:
<
<
Bem vindo à página da edição de 2009/10 da disciplina de Cálculo de Programas.
>
>
Bem vindo à página da edição de 2010/11 da disciplina de Cálculo de Programas.
 O meu nome é José Nuno Oliveira e sou o responsável por esta disciplina, que conta com uma
Changed:
<
<
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que se leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
>
>
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que se leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
 TFM09.jpg Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais de programação desde há mais de 25 anos.
Line: 16 to 16
 A Universidade do Minho tem uma longa tradição neste tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de
Changed:
<
<
Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.
>
>
Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não tem de facto.
 
<-- O que queremos é singularmente captado pelo selo !-->


WebHome 27 - 11 Jul 2010 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2009/10 da disciplina de Cálculo de Programas. O meu nome é José Nuno Oliveira e sou o responsável por esta disciplina, que conta com uma

Changed:
<
<
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
>
>
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que se leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
 TFM09.jpg Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais de programação desde há mais de 25 anos.

WebHome 26 - 05 Jul 2010 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2009/10 da disciplina de Cálculo de Programas.

Line: 10 to 10
 A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.
Changed:
<
<
Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros subtis cujos testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.
>
>
Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros subtis que os testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.
 Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.

WebHome 25 - 01 Jun 2010 - Main.JoseNunoOliveira
Line: 1 to 1
 

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2009/10 da disciplina de Cálculo de Programas. O meu nome é José Nuno Oliveira e sou o responsável por esta disciplina, que conta com uma

Changed:
<
<
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que ensinam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
>
>
equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software.
 TFM09.jpg Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais de programação desde há mais de 25 anos.
Line: 15 to 15
 Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.

A Universidade do Minho tem uma longa tradição neste tipo de ensino.

Changed:
<
<
Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.
>
>
Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.
 
<-- O que queremos é singularmente captado pelo selo !-->


WebHome 24 - 28 May 2010 - Main.JoseNunoOliveira
Line: 1 to 1
Changed:
<
<

Motivação

>
>

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2009/10 da disciplina de Cálculo de Programas. O meu nome é José Nuno Oliveira e sou o responsável por esta disciplina, que conta com uma equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que ensinam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software. TFM09.jpg Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais de programação desde há mais de 25 anos.

 A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.
Line: 39 to 45
 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"
META FILEATTACHMENT attachment="manelinho1.JPG" attr="h" comment="" date="1236942730" name="manelinho1.JPG" path="manelinho1.JPG" size="189062" stream="manelinho1.JPG" user="Main.AlcinoCunha" version="1"
Added:
>
>
META FILEATTACHMENT attachment="portrait.png" attr="h" comment="" date="1275057461" name="portrait.png" path="portrait.png" size="32096" stream="portrait.png" user="Main.JoseNunoOliveira" version="1"

WebHome 23 - 24 Feb 2010 - Main.JoseNunoOliveira
Line: 1 to 1
Deleted:
<
<
 

Motivação

A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.

Changed:
<
<
Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros cujos testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.
>
>
Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros subtis cujos testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.
 
Changed:
<
<
Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a correcção fique comprometida.
>
>
Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.
 
Changed:
<
<
A Universidade do Minho tem uma longa tradição nesse tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina essa disciplina. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.
>
>
A Universidade do Minho tem uma longa tradição neste tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.
 
<-- O que queremos é singularmente captado pelo selo !-->


WebHome 22 - 23 Feb 2010 - Main.JoseNunoOliveira
Line: 1 to 1
 
Added:
>
>

Motivação

 
Changed:
<
<

Página principal

>
>
A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.

Tratando-se de programas de computador, essa sugestão é da maior importância: os programas escritos sem se pensar antes têm normalmente erros cujos testes não detectam e que constituem não só um perigo (por exemplo, em software crítico) mas também um custo acrescido para as empresas que os desenvolvem.

Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma a evitar tais erros. Para isso, é preciso introduzir a noção de cálculo em programação, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a correcção fique comprometida.

A Universidade do Minho tem uma longa tradição nesse tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina essa disciplina. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não sabe de facto.

<-- O que queremos é singularmente captado pelo selo !-->
 
Deleted:
<
<
Entrar aqui.
 

Resultados da Aprendizagem

Line: 22 to 32
 
  • Programação funcional avançada: construir e raciocinar sobre programas funcionais com efeitos sob a forma de mónades.
Added:
>
>

Página principal

Entrar aqui.

 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 21 - 19 Feb 2010 - Main.JoseNunoOliveira
Line: 1 to 1
Changed:
<
<
Dès le commencement de ce siècle, l'algorithme avait atteint un degré de complication tel que tout progrès était devenu impossible par ce moyen, sans l'élégance que les géomètres modernes ont su imprimer à leurs recherches, et au moyen de laquelle l'esprit saisit promptement et d'un seul coup un grand nombre d'opérations.

Il est évident que l'élégance si vantée et à si juste titre, n'a pas d'autre but...

Sauter à pieds joints sur ces calculs; grouper les opérations, les classer suivant leurs difficultés et non suivant leurs formes; telle est, suivant moi, la mission des géomètres futurs; telle est la voie où je suis entré dans cet ouvrage.



Simplicity does not precede complexity, but follows it.
>
>

Página principal

Entrar aqui.

Resultados da Aprendizagem

 
Changed:
<
<
Alan Perlis 1982
>
>
Quien sabe por Algebra, sabe scientificamente.
Pedro Nunes(1502-1578) in Libro de Algebra, 1567, fol 270r.

  • Análise de programas: escrever programas funcionais com recurso a combinadores algébricos.

  • Transformação de programas: recurso à algebra da programação para se obterem programas mais eficientes a partir de outros.

  • Compreensão de programas: recurso à factorização em pares "fold" + "unfold" (hilomorfismos) como forma de se perceber o significado de um programa funcional.

  • Síntese de programas: cálculo de ciclos-for a partir de definições indutivas da matemática.
 
Added:
>
>
  • Programação funcional avançada: construir e raciocinar sobre programas funcionais com efeitos sob a forma de mónades.
 
Deleted:
<
<

 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 20 - 01 Apr 2009 - Main.AlcinoCunha
Line: 1 to 1
 
Dès le commencement de ce siècle, l'algorithme avait atteint un degré de complication tel que tout progrès était devenu impossible par ce moyen, sans l'élégance que les géomètres modernes ont su imprimer à leurs recherches, et au moyen de laquelle l'esprit saisit promptement et d'un seul coup un grand nombre d'opérations.
Line: 20 to 20
 


Deleted:
<
<

Manelinho

 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 19 - 13 Mar 2009 - Main.AlcinoCunha
Line: 1 to 1
 
Dès le commencement de ce siècle, l'algorithme avait atteint un degré de complication tel que tout progrès était devenu impossible par ce moyen, sans l'élégance que les géomètres modernes ont su imprimer à leurs recherches, et au moyen de laquelle l'esprit saisit promptement et d'un seul coup un grand nombre d'opérations.
Changed:
<
<
Il est évident que l'élégance si vantée et à si juste titre, n'a pas d'autre but.

...

>
>
Il est évident que l'élégance si vantée et à si juste titre, n'a pas d'autre but...
 Sauter à pieds joints sur ces calculs; grouper les opérations, les classer suivant leurs difficultés et non suivant leurs formes; telle est, suivant moi, la mission des géomètres futurs; telle est la voie où je suis entré dans cet ouvrage.

WebHome 18 - 13 Mar 2009 - Main.AlcinoCunha
Line: 1 to 1
 
Dès le commencement de ce siècle, l'algorithme avait atteint un degré de complication tel que tout progrès était devenu impossible par ce moyen, sans l'élégance que les géomètres modernes ont su imprimer à leurs recherches, et au moyen de laquelle l'esprit saisit promptement et d'un seul coup un grand nombre d'opérations.
Line: 9 to 9
 Sauter à pieds joints sur ces calculs; grouper les opérations, les classer suivant leurs difficultés et non suivant leurs formes; telle est, suivant moi, la mission des géomètres futurs; telle est la voie où je suis entré dans cet ouvrage.
Deleted:
<
<

 
Added:
>
>


Simplicity does not precede complexity, but follows it.


 
Added:
>
>
Manelinho
 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"
Added:
>
>
META FILEATTACHMENT attachment="manelinho1.JPG" attr="h" comment="" date="1236942730" name="manelinho1.JPG" path="manelinho1.JPG" size="189062" stream="manelinho1.JPG" user="Main.AlcinoCunha" version="1"

WebHome 17 - 28 Feb 2008 - Main.AlcinoCunha
Line: 1 to 1
Changed:
<
<
Since the beginning of the century, computational procedures have become so complicated that any progress by those means has become impossible, without the elegance which modern mathematicians have brought to bear on their research, and by means of which the spirit comprehends quickly and in one step a great many computations.
>
>
Dès le commencement de ce siècle, l'algorithme avait atteint un degré de complication tel que tout progrès était devenu impossible par ce moyen, sans l'élégance que les géomètres modernes ont su imprimer à leurs recherches, et au moyen de laquelle l'esprit saisit promptement et d'un seul coup un grand nombre d'opérations.
 
Changed:
<
<
It is clear that elegance, so vaunted and so aptly named, can have no other purpose...
>
>
Il est évident que l'élégance si vantée et à si juste titre, n'a pas d'autre but.
 
Changed:
<
<
Go to the roots of these calculations! Group the operations. Classify them according to their complexities rather than their appearances! This, I believe, is the mission of future mathematicians. This is the road on which I am embarking in this work.
>
>
...

Sauter à pieds joints sur ces calculs; grouper les opérations, les classer suivant leurs difficultés et non suivant leurs formes; telle est, suivant moi, la mission des géomètres futurs; telle est la voie où je suis entré dans cet ouvrage.

 
Changed:
<
<
Évariste Galois. 1832.
>
>
Évariste Galois 1832
 

META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"

WebHome 16 - 27 Feb 2008 - Main.AlcinoCunha
Line: 1 to 1
 
Since the beginning of the century, computational procedures have become so complicated that any progress by those means has become impossible, without the elegance which modern mathematicians have brought to bear on their research, and by means of which the spirit comprehends quickly and in one step a great many computations.

It is clear that elegance, so vaunted and so aptly named, can have no other purpose...


WebHome 15 - 19 Feb 2008 - Main.AlcinoCunha
Line: 1 to 1
Added:
>
>
Since the beginning of the century, computational procedures have become so complicated that any progress by those means has become impossible, without the elegance which modern mathematicians have brought to bear on their research, and by means of which the spirit comprehends quickly and in one step a great many computations.

It is clear that elegance, so vaunted and so aptly named, can have no other purpose...

Go to the roots of these calculations! Group the operations. Classify them according to their complexities rather than their appearances! This, I believe, is the mission of future mathematicians. This is the road on which I am embarking in this work.


 
Deleted:
<
<
Manuel Alcino Cunha
 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 14 - 19 Feb 2008 - Main.AlcinoCunha
Line: 1 to 1
Deleted:
<
<
Esta disciplina tem por objectivo introduzir técnicas de modelação e análise de sistemas concorrentes ou reactivos. Serão apresentadas duas abordagens distintas a este problema.
 
Changed:
<
<
A primeira baseia-se na utilização de redes de Petri e lógica temporal. As redes de Petri são um modelo gráfico muito poderoso para representar sistemas concorrentes de média e alta complexidade. Algumas propriedades de sistemas concorrentes podem ser verificadas com técnicas de análise directa das redes, mas para especificar propriedades mais complexas será introduzida a lógica temporal. Esta lógica possui operadores modais específicos que nos permitem descrever a evolução do estado da computação ao longo do tempo. Em particular, será utilizada a lógica de tempo ramificado CTL, para a qual serão apresentadas diferentes técnicas de verificação de modelos. Esta abordagem será aplicada na modelação e análise de algoritmos clássicos da programação concorrente, protocolos de comunicação simples, e sistemas de controle de produção. Na componente prática laboratorial serão utilizadas ferramentas para edição gráfica de redes de Petri e para verificação simbólica de modelos.

Muitos modelos para a computação reactiva evoluiram a partir da noção de autómato, da qual retêm a estrutura de transições etiquetadas --- precisamente pelas interacções em que o sistema se envolve. Tais sistemas exibem comportamentos --- usualmente designados por processos --- que podem ser descritos por linguagens formais e que, mais importante ainda, formam domínios nos quais se podem definir (ou identificar) determinadas estruturas algébricas. I.e., operadores que os combinam e que exibem um conjunto suficientemente rico de propriedades que permitem combinar os padrões de interacção dos vários sistemas em presença. É esta a área de um conjunto de abordagems que exploram a estrutura algébrica dos comportamentos de sistemas reactivos e que se popularizou, a partir de finais dos anos '70 sob a designação de álgebras de processos.

A segunda parte desta disciplina recorre precisamente a duas álgebras de processos (o CCS e o cálculo Pi) para modelar as interacções e evolução dos sistemas reactivos, estudar a sua composicionalidade, definir equivalências entre eles, identificar propriedades e raciocinar equacionalmente sobre elas. O cálculo Pi, em particular, irá permitir-nos discutir formalmente acerca de sistemas reactivos cuja estrutura de interacções se altera dinamicamente ao longo da computação.

Manuel Alcino Cunha
Luís Soares Barbosa

>
>
Manuel Alcino Cunha
 
META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 13 - 30 Apr 2007 - Main.LuisSoaresBarbosa
Line: 1 to 1
 Esta disciplina tem por objectivo introduzir técnicas de modelação e análise de sistemas concorrentes ou reactivos. Serão apresentadas duas abordagens distintas a este problema.

A primeira baseia-se na utilização de redes de Petri e lógica temporal. As redes de Petri são um modelo gráfico muito poderoso para representar sistemas concorrentes de média e alta complexidade. Algumas propriedades de sistemas concorrentes podem ser verificadas com técnicas de análise directa das redes, mas para especificar propriedades mais complexas será introduzida a lógica temporal. Esta lógica possui operadores modais específicos que nos permitem descrever a evolução do estado da computação ao longo do tempo. Em particular, será utilizada a lógica de tempo ramificado CTL, para a qual serão apresentadas diferentes técnicas de verificação de modelos. Esta abordagem será aplicada na modelação e análise de algoritmos clássicos da programação concorrente, protocolos de comunicação simples, e sistemas de controle de produção. Na componente prática laboratorial serão utilizadas ferramentas para edição gráfica de redes de Petri e para verificação simbólica de modelos.

Line: 29 to 29
 Luís Soares Barbosa

META FILEATTACHMENT attachment="petri.tiff" attr="h" comment="" date="1171385285" name="petri.tiff" path="petri.tiff" size="40028" stream="petri.tiff" user="Main.AlcinoCunha" version="3"
Added:
>
>
META FILEATTACHMENT attachment="Lic3.pdf" attr="h" comment="" date="1177929558" name="Lic3.pdf" path="Lic3.pdf" size="332988" stream="Lic3.pdf" user="Main.LuisSoaresBarbosa" version="2"

WebHome 12 - 21 Feb 2007 - Main.AlcinoCunha

WebHome 11 - 22 Feb 2011 - Main.TWikiGuest

WebHome 10 - 22 Feb 2011 - Main.TWikiGuest

WebHome 9 - 22 Feb 2011 - Main.TWikiGuest

WebHome 8 - 22 Feb 2011 - Main.TWikiGuest

WebHome 7 - 22 Feb 2011 - Main.TWikiGuest

WebHome 6 - 22 Feb 2011 - Main.TWikiGuest

WebHome 5 - 22 Feb 2011 - Main.TWikiGuest

WebHome 4 - 22 Feb 2011 - Main.TWikiGuest

WebHome 3 - 22 Feb 2011 - Main.TWikiGuest

WebHome 2 - 22 Feb 2011 - Main.TWikiGuest

WebHome 1 - 22 Feb 2011 - Main.TWikiGuest
Line: 1 to 1

Revision 30r30 - 22 Feb 2011 - 14:06:30 - JoseNunoOliveira
Revision 29r29 - 15 Feb 2011 - 14:07:39 - JoseNunoOliveira
Revision 28r28 - 15 Feb 2011 - 11:50:56 - JoseNunoOliveira
Revision 27r27 - 11 Jul 2010 - 10:33:38 - JoseNunoOliveira
Revision 26r26 - 05 Jul 2010 - 17:05:29 - JoseNunoOliveira
Revision 25r25 - 01 Jun 2010 - 10:28:50 - JoseNunoOliveira
Revision 24r24 - 28 May 2010 - 14:46:48 - JoseNunoOliveira
Revision 23r23 - 24 Feb 2010 - 16:04:49 - JoseNunoOliveira
Revision 22r22 - 23 Feb 2010 - 13:43:57 - JoseNunoOliveira
Revision 21r21 - 19 Feb 2010 - 17:09:06 - JoseNunoOliveira
Revision 20r20 - 01 Apr 2009 - 11:42:19 - AlcinoCunha
Revision 19r19 - 13 Mar 2009 - 19:20:16 - AlcinoCunha
Revision 18r18 - 13 Mar 2009 - 11:25:33 - AlcinoCunha
Revision 17r17 - 28 Feb 2008 - 16:14:16 - AlcinoCunha
Revision 16r16 - 27 Feb 2008 - 22:37:29 - AlcinoCunha
Revision 15r15 - 19 Feb 2008 - 16:32:13 - AlcinoCunha
Revision 14r14 - 19 Feb 2008 - 15:02:18 - AlcinoCunha
Revision 13r13 - 30 Apr 2007 - 10:39:22 - LuisSoaresBarbosa
Revision 12r12 - 21 Feb 2007 - 22:40:11 - AlcinoCunha
Revision 11r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 10r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 9r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 8r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 7r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 6r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 5r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 4r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 3r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 2r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
Revision 1r1 - 22 Feb 2011 - 14:06:30 - TWikiGuest
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM