1,720,976 research outputs found
Static verification of data races in openMP
No full textTese de mestrado em Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014Com o uso de linguagens paralelas nascem alguns problemas como data race , uma argura para os programadores durante o seu trabalho. Data race são quando dois ou mais threads em um único processo acedem a mesma posic¸ ão de memória ao mesmo tempo, sendo que um ou mais acessos são para a escrita/leitura, sem sincronização adequada. A nossa ferramenta (SVDR: Static Verification of Data race in OpenMP) foi desenvolvida com o propósito de verificar a ausência de data races em OpenMP (uma linguagem de programac¸ ão paralela). Empregamos a verificação estática com intençãoo de encontrar data races sem necessariamente executar o programa, possibilitando dessa forma ao utilizador, encontrar o problema antes de receber o resultado do mesmo. Para melhor compreensão de como funciona a ferramenta, é pertinente apresentar de forma concisa, as linguagens de programac¸ ˜ao aqui abordadas: OpenMP e Boogie. OpenMP (Aberto Multi-Processing) 2.1 ´e um API usado na programação (C, Fortran, C++) em multiprocessadores com memória partilhada em multiplataformas e funciona em quase todos Sistemas operativos e arquitecturas. Boogie [2, 17] ´e uma linguagem de verificação intermédia, projectada como uma camada sobre a qual é possível construir outros verificadores para outras línguaguens. Uma vez aclaradas as definições, é mais fácil contextualizar e compreender como a ferramenta funciona. Como já foi referido previamente, o objectivo da ferramenta é traduzir código OpenMP em código Boogie com o propósito de verificar se existe ou não data race no ficheiro de entrada. Assim sendo, é possível aferir que existem duas etapas para o processo de verificação: a primeira é a tradução de OpenMP em Boogie, e a segunda é a verificação de data race no ficheiro de entrada - que é do tipo bpl, ou seja, código Boogie. A primeira fase não é tratado pela ferramenta, de modo que é necessária uma tradução manual do código OpenMP para o código Boogie. A segunda fase é a ferramenta que foi implementada, SVDR. O SVDR funciona da seguinte forma: recebe como entrada um ficheiro bpl (um OpenMP traduzido em código Boogie) e retorna como resultado um ficheiro bpl com o algoritmo necessário para verificar se há ou não um data race no ficheiro de entrada. O algoritmo criado é baseado no uso de não determinismo, invariantes e assertions. Este funciona do seguinte modo, para verificar a existência de data race num ciclo While, o que se faz é guardar numa variável global, que designamos de current off, o valor actual do índice do array (independentemente de se tratar de uma leitura ou uma escrita, o processo é o mesmo), e atribuir a outra variável global, que denominamos de current,o valor de true. Após guardados os referidos valores, o que se faz a seguir, é a incrementação do ciclo, atribuímos os valores do current e do current off a duas novas variáveis globais previous e previous off. Estas atribuições são feitas para evitar que se aceda duas vezes seguidas a mesma posição, porque isso poderia conduzir a data race. Tanto as atribuições de current como de previous, são feitas dentro de if não determinísticos. Não determinismo é por definição “Uma propriedade da computação na qual pode ter um ou mais resultados”, mas neste caso especifico significa que não é possível saber se entra ou não no if. A razão para o seu uso, é apenas a não necessidade, neste caso, de se guardar todos os valores do currrent, e mudar todos os valores do previous (até porque se tivermos em consideração todas as possibilidade de execução do programa, haverá sempre uma para cada tarefa). Depois de guardados os valores é necessário validá-los de alguma forma, até porque senão, seriam apenas if num programa, ou seja, não teriam nenhum efeito especifico. A modo utilizado para verificar, é empregando assercoes, ou seja, criamos um assert na qual se afirma que caso o previous seja verdadeiro, então o previous off será sempre diferente do índex actual do vector. Caso isto seja verdade, ou seja, caso se ocorra no programa a veracidade dessa afirmação, então não existem data race, caso contrário, existem. Mas para que esse assert seja sempre verdade, durante o programa, é indispensável a criação de uma invariant para suportar a sua veracidade. No nosso caso, as invariantes são testadas usando Houdini 2.2. São criadas bases de invariantes pela ferramenta, que posteriormente ao realizar-se a verificação do ficheiro com o algoritmo no Verificador Boogie, adiciona um atributo relativo ao Houdini. Por fim, para saber se existe ou não data race no código, utilizamos o Verificador Boogie para atestar o programa com o algoritmo. Como conclusão, o que se pode dizer é que a ferramenta apresentou resultados bastante satisfatórios, e que em todos os exemplos apresentados e testados, o efeito foi o esperado. Apesar de algumas limitações, a ferramenta cumpre com o que foi descrito anteriormente Verifica estaticamente a existência de data race na linguagem OpenMP.Increasingly, programmers use multi-core processors to develop code with multiple threads, i.e, parallel programs. There are some tools that support parallelism such as Intel Parallel Lint 2.4.1 or Intel Thread checker 2.4.2 and some parallel programming languages such as OpenMP 2.1. With the use of parallel languages emerged some problems such as data races that no programmer likes to come across when working. Data races are when two or more threads in a single process access the same memory location concurrently and one or more of the accesses are for writing without proper synchronization. Our tool (SVDR: Static Verification of Data race in OpenMP) was developed with the intention to verify data race freedom in OpenMP (a parallel programming language). We used static verification because we wanted to try to find data races without running the program because that way the user discovers the problem before getting results from the program. The SVDR tool works as follows: it receives as input a bpl file (a file with the translated OpenMP code into Boogie code), then the tool performs executes the algorithm on the input, and gives as output the execution, i.e, the Boogie code with the algorithm necessary to verify if there is or not a data race. Next the output of the SVDR is going to be used as input in the Boogie Verifier that will determine whether or not there exists a data race in the input. If there is a data race then the verifier will give an error, otherwise the verifier will verifies the code without any problem. After several tests it was possible for us to verify that the tool works correctly in all tests that we ran. The examples that we ran were with nested loops, but just one of them was parallel, and also with simple loops, with reads and writes, and all of the examples were verified as expected by the Boogie Verifier. The tool is useful to help the user to verify is exists any data race problem in code so that they can solve the problem if it exists
Session Types in Concurrent Calculi: Higher-Order Processes and Objects
Get PDFThis dissertation investigates different formalisms, in the form of programming language calculi,
that are aimed at providing a theoretical foundation for structured concurrent programming based
on session types. The structure of a session type is essentially a process-algebraic style description
of the behaviour of a single program identifier serving as a communication medium (and usually
referred to as a channel): the types incorporate typed inputs, outputs, and choices which can be
composed to form larger protocol descriptions. The effectiveness of session typing can be attributed
to the linear treatment of channels and session types, and to the use of tractable methods
such as syntactic duality to decide if the types of two connected channels are compatible. Linearity
is ensured when accumulating the uses of a channel into a composite type that describes also
the order of those actions. Duality provides a tractable and intuitive method for deciding when
two connected channels can interact and exchange values in a statically determined type-safe way.
We present our contributions to the theory of sessions, distilled into two families of programming
calculi, the first based on higher-order processes and the second based on objects. Our work unifies,
improves and extends, in manifold ways, the session primitives and typing systems for the
Lambda-calculus, the Pi-calculus, the Object-calculus, and their combinations in multi-paradigm
languages. Of particular interest are: the treatment of infinite interactions expressed with recursive
sessions; the capacity to encapsulate channels in higher-order structures which can be exchanged
and kept suspended, i.e., the use of code as data; the integration of protocol structure directly
into the description of objects, providing a powerful and uniformly extensible set of implementation
abstractions; finally, the introduction of asynchronous subtyping, which enables controlled
reordering of actions on either side of a session. Our work on higher-order processes and on object
calculi for session-based concurrent programming provides a theoretical foundation for programming
language design integrating functional, process, and object-oriented features
Static verification of data races in openMP
No full textTese de mestrado em Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014Com o uso de linguagens paralelas nascem alguns problemas como data race , uma argura para os programadores durante o seu trabalho. Data race são quando dois ou mais threads em um único processo acedem a mesma posic¸ ão de memória ao mesmo tempo, sendo que um ou mais acessos são para a escrita/leitura, sem sincronização adequada. A nossa ferramenta (SVDR: Static Verification of Data race in OpenMP) foi desenvolvida com o propósito de verificar a ausência de data races em OpenMP (uma linguagem de programac¸ ão paralela). Empregamos a verificação estática com intençãoo de encontrar data races sem necessariamente executar o programa, possibilitando dessa forma ao utilizador, encontrar o problema antes de receber o resultado do mesmo. Para melhor compreensão de como funciona a ferramenta, é pertinente apresentar de forma concisa, as linguagens de programac¸ ˜ao aqui abordadas: OpenMP e Boogie. OpenMP (Aberto Multi-Processing) 2.1 ´e um API usado na programação (C, Fortran, C++) em multiprocessadores com memória partilhada em multiplataformas e funciona em quase todos Sistemas operativos e arquitecturas. Boogie [2, 17] ´e uma linguagem de verificação intermédia, projectada como uma camada sobre a qual é possível construir outros verificadores para outras línguaguens. Uma vez aclaradas as definições, é mais fácil contextualizar e compreender como a ferramenta funciona. Como já foi referido previamente, o objectivo da ferramenta é traduzir código OpenMP em código Boogie com o propósito de verificar se existe ou não data race no ficheiro de entrada. Assim sendo, é possível aferir que existem duas etapas para o processo de verificação: a primeira é a tradução de OpenMP em Boogie, e a segunda é a verificação de data race no ficheiro de entrada - que é do tipo bpl, ou seja, código Boogie. A primeira fase não é tratado pela ferramenta, de modo que é necessária uma tradução manual do código OpenMP para o código Boogie. A segunda fase é a ferramenta que foi implementada, SVDR. O SVDR funciona da seguinte forma: recebe como entrada um ficheiro bpl (um OpenMP traduzido em código Boogie) e retorna como resultado um ficheiro bpl com o algoritmo necessário para verificar se há ou não um data race no ficheiro de entrada. O algoritmo criado é baseado no uso de não determinismo, invariantes e assertions. Este funciona do seguinte modo, para verificar a existência de data race num ciclo While, o que se faz é guardar numa variável global, que designamos de current off, o valor actual do índice do array (independentemente de se tratar de uma leitura ou uma escrita, o processo é o mesmo), e atribuir a outra variável global, que denominamos de current,o valor de true. Após guardados os referidos valores, o que se faz a seguir, é a incrementação do ciclo, atribuímos os valores do current e do current off a duas novas variáveis globais previous e previous off. Estas atribuições são feitas para evitar que se aceda duas vezes seguidas a mesma posição, porque isso poderia conduzir a data race. Tanto as atribuições de current como de previous, são feitas dentro de if não determinísticos. Não determinismo é por definição “Uma propriedade da computação na qual pode ter um ou mais resultados”, mas neste caso especifico significa que não é possível saber se entra ou não no if. A razão para o seu uso, é apenas a não necessidade, neste caso, de se guardar todos os valores do currrent, e mudar todos os valores do previous (até porque se tivermos em consideração todas as possibilidade de execução do programa, haverá sempre uma para cada tarefa). Depois de guardados os valores é necessário validá-los de alguma forma, até porque senão, seriam apenas if num programa, ou seja, não teriam nenhum efeito especifico. A modo utilizado para verificar, é empregando assercoes, ou seja, criamos um assert na qual se afirma que caso o previous seja verdadeiro, então o previous off será sempre diferente do índex actual do vector. Caso isto seja verdade, ou seja, caso se ocorra no programa a veracidade dessa afirmação, então não existem data race, caso contrário, existem. Mas para que esse assert seja sempre verdade, durante o programa, é indispensável a criação de uma invariant para suportar a sua veracidade. No nosso caso, as invariantes são testadas usando Houdini 2.2. São criadas bases de invariantes pela ferramenta, que posteriormente ao realizar-se a verificação do ficheiro com o algoritmo no Verificador Boogie, adiciona um atributo relativo ao Houdini. Por fim, para saber se existe ou não data race no código, utilizamos o Verificador Boogie para atestar o programa com o algoritmo. Como conclusão, o que se pode dizer é que a ferramenta apresentou resultados bastante satisfatórios, e que em todos os exemplos apresentados e testados, o efeito foi o esperado. Apesar de algumas limitações, a ferramenta cumpre com o que foi descrito anteriormente Verifica estaticamente a existência de data race na linguagem OpenMP.Increasingly, programmers use multi-core processors to develop code with multiple threads, i.e, parallel programs. There are some tools that support parallelism such as Intel Parallel Lint 2.4.1 or Intel Thread checker 2.4.2 and some parallel programming languages such as OpenMP 2.1. With the use of parallel languages emerged some problems such as data races that no programmer likes to come across when working. Data races are when two or more threads in a single process access the same memory location concurrently and one or more of the accesses are for writing without proper synchronization. Our tool (SVDR: Static Verification of Data race in OpenMP) was developed with the intention to verify data race freedom in OpenMP (a parallel programming language). We used static verification because we wanted to try to find data races without running the program because that way the user discovers the problem before getting results from the program. The SVDR tool works as follows: it receives as input a bpl file (a file with the translated OpenMP code into Boogie code), then the tool performs executes the algorithm on the input, and gives as output the execution, i.e, the Boogie code with the algorithm necessary to verify if there is or not a data race. Next the output of the SVDR is going to be used as input in the Boogie Verifier that will determine whether or not there exists a data race in the input. If there is a data race then the verifier will give an error, otherwise the verifier will verifies the code without any problem. After several tests it was possible for us to verify that the tool works correctly in all tests that we ran. The examples that we ran were with nested loops, but just one of them was parallel, and also with simple loops, with reads and writes, and all of the examples were verified as expected by the Boogie Verifier. The tool is useful to help the user to verify is exists any data race problem in code so that they can solve the problem if it exists
Static verification of data races in openMP
No full textTese de mestrado em Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014Com o uso de linguagens paralelas nascem alguns problemas como data race , uma argura para os programadores durante o seu trabalho. Data race são quando dois ou mais threads em um único processo acedem a mesma posic¸ ão de memória ao mesmo tempo, sendo que um ou mais acessos são para a escrita/leitura, sem sincronização adequada. A nossa ferramenta (SVDR: Static Verification of Data race in OpenMP) foi desenvolvida com o propósito de verificar a ausência de data races em OpenMP (uma linguagem de programac¸ ão paralela). Empregamos a verificação estática com intençãoo de encontrar data races sem necessariamente executar o programa, possibilitando dessa forma ao utilizador, encontrar o problema antes de receber o resultado do mesmo. Para melhor compreensão de como funciona a ferramenta, é pertinente apresentar de forma concisa, as linguagens de programac¸ ˜ao aqui abordadas: OpenMP e Boogie. OpenMP (Aberto Multi-Processing) 2.1 ´e um API usado na programação (C, Fortran, C++) em multiprocessadores com memória partilhada em multiplataformas e funciona em quase todos Sistemas operativos e arquitecturas. Boogie [2, 17] ´e uma linguagem de verificação intermédia, projectada como uma camada sobre a qual é possível construir outros verificadores para outras línguaguens. Uma vez aclaradas as definições, é mais fácil contextualizar e compreender como a ferramenta funciona. Como já foi referido previamente, o objectivo da ferramenta é traduzir código OpenMP em código Boogie com o propósito de verificar se existe ou não data race no ficheiro de entrada. Assim sendo, é possível aferir que existem duas etapas para o processo de verificação: a primeira é a tradução de OpenMP em Boogie, e a segunda é a verificação de data race no ficheiro de entrada - que é do tipo bpl, ou seja, código Boogie. A primeira fase não é tratado pela ferramenta, de modo que é necessária uma tradução manual do código OpenMP para o código Boogie. A segunda fase é a ferramenta que foi implementada, SVDR. O SVDR funciona da seguinte forma: recebe como entrada um ficheiro bpl (um OpenMP traduzido em código Boogie) e retorna como resultado um ficheiro bpl com o algoritmo necessário para verificar se há ou não um data race no ficheiro de entrada. O algoritmo criado é baseado no uso de não determinismo, invariantes e assertions. Este funciona do seguinte modo, para verificar a existência de data race num ciclo While, o que se faz é guardar numa variável global, que designamos de current off, o valor actual do índice do array (independentemente de se tratar de uma leitura ou uma escrita, o processo é o mesmo), e atribuir a outra variável global, que denominamos de current,o valor de true. Após guardados os referidos valores, o que se faz a seguir, é a incrementação do ciclo, atribuímos os valores do current e do current off a duas novas variáveis globais previous e previous off. Estas atribuições são feitas para evitar que se aceda duas vezes seguidas a mesma posição, porque isso poderia conduzir a data race. Tanto as atribuições de current como de previous, são feitas dentro de if não determinísticos. Não determinismo é por definição “Uma propriedade da computação na qual pode ter um ou mais resultados”, mas neste caso especifico significa que não é possível saber se entra ou não no if. A razão para o seu uso, é apenas a não necessidade, neste caso, de se guardar todos os valores do currrent, e mudar todos os valores do previous (até porque se tivermos em consideração todas as possibilidade de execução do programa, haverá sempre uma para cada tarefa). Depois de guardados os valores é necessário validá-los de alguma forma, até porque senão, seriam apenas if num programa, ou seja, não teriam nenhum efeito especifico. A modo utilizado para verificar, é empregando assercoes, ou seja, criamos um assert na qual se afirma que caso o previous seja verdadeiro, então o previous off será sempre diferente do índex actual do vector. Caso isto seja verdade, ou seja, caso se ocorra no programa a veracidade dessa afirmação, então não existem data race, caso contrário, existem. Mas para que esse assert seja sempre verdade, durante o programa, é indispensável a criação de uma invariant para suportar a sua veracidade. No nosso caso, as invariantes são testadas usando Houdini 2.2. São criadas bases de invariantes pela ferramenta, que posteriormente ao realizar-se a verificação do ficheiro com o algoritmo no Verificador Boogie, adiciona um atributo relativo ao Houdini. Por fim, para saber se existe ou não data race no código, utilizamos o Verificador Boogie para atestar o programa com o algoritmo. Como conclusão, o que se pode dizer é que a ferramenta apresentou resultados bastante satisfatórios, e que em todos os exemplos apresentados e testados, o efeito foi o esperado. Apesar de algumas limitações, a ferramenta cumpre com o que foi descrito anteriormente Verifica estaticamente a existência de data race na linguagem OpenMP.Increasingly, programmers use multi-core processors to develop code with multiple threads, i.e, parallel programs. There are some tools that support parallelism such as Intel Parallel Lint 2.4.1 or Intel Thread checker 2.4.2 and some parallel programming languages such as OpenMP 2.1. With the use of parallel languages emerged some problems such as data races that no programmer likes to come across when working. Data races are when two or more threads in a single process access the same memory location concurrently and one or more of the accesses are for writing without proper synchronization. Our tool (SVDR: Static Verification of Data race in OpenMP) was developed with the intention to verify data race freedom in OpenMP (a parallel programming language). We used static verification because we wanted to try to find data races without running the program because that way the user discovers the problem before getting results from the program. The SVDR tool works as follows: it receives as input a bpl file (a file with the translated OpenMP code into Boogie code), then the tool performs executes the algorithm on the input, and gives as output the execution, i.e, the Boogie code with the algorithm necessary to verify if there is or not a data race. Next the output of the SVDR is going to be used as input in the Boogie Verifier that will determine whether or not there exists a data race in the input. If there is a data race then the verifier will give an error, otherwise the verifier will verifies the code without any problem. After several tests it was possible for us to verify that the tool works correctly in all tests that we ran. The examples that we ran were with nested loops, but just one of them was parallel, and also with simple loops, with reads and writes, and all of the examples were verified as expected by the Boogie Verifier. The tool is useful to help the user to verify is exists any data race problem in code so that they can solve the problem if it exists
Proof Nets as Processes
No full textThis work describes a process algebraic interpretation of Proof-nets, which are the canonical objects of Linear Logic proofs. It therefore offers a logically founded basis for deterministic, implicit parallelism.We present delta-calculus, a novel interpretation of Linear Logic, in the form of a typed process algebra that enjoys a Curry-Howard correspondence with Proof Nets. Reduction inherits the qualities of the logical objects: termination, deadlock-freedom, determinism, and very importantly, a high degree of parallelism. We obtain the necessary soundness results and provide a propositions-as-types theorem. The basic system is extended in two directions. First, we adapt it to interpret Affine Logic. Second, we propose extensions for general recursion, and introduce a novel form of recursive linear types. As an application we show a highly parallel type-preserving translation from a linear System F and extend it to the recursive variation. Our interpretation can be seen as a more canonical proof-theoretic alternative to several recent works on pi-calculus interpretations of linear sequent proofs (propositions-as-sessions) which exhibit reduced parallelism
Proof Nets as Processes
No full textThis work describes a process algebraic interpretation of Proof-nets, which are the canonical objects of Linear Logic proofs. It therefore offers a logically founded basis for deterministic, implicit parallelism.We present delta-calculus, a novel interpretation of Linear Logic, in the form of a typed process algebra that enjoys a Curry-Howard correspondence with Proof Nets. Reduction inherits the qualities of the logical objects: termination, deadlock-freedom, determinism, and very importantly, a high degree of parallelism. We obtain the necessary soundness results and provide a propositions-as-types theorem. The basic system is extended in two directions. First, we adapt it to interpret Affine Logic. Second, we propose extensions for general recursion, and introduce a novel form of recursive linear types. As an application we show a highly parallel type-preserving translation from a linear System F and extend it to the recursive variation. Our interpretation can be seen as a more canonical proof-theoretic alternative to several recent works on pi-calculus interpretations of linear sequent proofs (propositions-as-sessions) which exhibit reduced parallelism
Proof Nets as Processes
No full textThis work describes a process algebraic interpretation of Proof-nets, which are the canonical objects of Linear Logic proofs. It therefore offers a logically founded basis for deterministic, implicit parallelism.We present delta-calculus, a novel interpretation of Linear Logic, in the form of a typed process algebra that enjoys a Curry-Howard correspondence with Proof Nets. Reduction inherits the qualities of the logical objects: termination, deadlock-freedom, determinism, and very importantly, a high degree of parallelism. We obtain the necessary soundness results and provide a propositions-as-types theorem. The basic system is extended in two directions. First, we adapt it to interpret Affine Logic. Second, we propose extensions for general recursion, and introduce a novel form of recursive linear types. As an application we show a highly parallel type-preserving translation from a linear System F and extend it to the recursive variation. Our interpretation can be seen as a more canonical proof-theoretic alternative to several recent works on pi-calculus interpretations of linear sequent proofs (propositions-as-sessions) which exhibit reduced parallelism
Aprendizagem baseada em projetos na consolidação de conceitos de programação de linguagens SCRIPT
No full textRelatório da prática de ensino supervisionada, Mestrado em Ensino de Informática, Universidade de Lisboa, 2014O presente relatório, elaborado no âmbito da unidade curricular de Introdução à Prática Profissional IV do Mestrado em Ensino de Informática da Universidade de Lisboa, refere-se à descrição da experiência da prática de ensino supervisionada realizada na Escola Secundária D. Dinis.
A intervenção foi realizada com uma turma do 12.ºAno do Curso Profissional Técnico de Gestão e Programação de Sistemas Informáticos, na disciplina de Programação e Sistemas de Informação, mais especificamente no módulo opcional de Ferramentas de Desenvolvimento de Páginas Web. Esta turma é constituída por 15 alunos do sexo masculino e apenas dois do sexo feminino.
Tendo como referência os objetivos estabelecidos para o referido módulo, foram abordados conceitos de linguagem de programação script, sistemas de gestão de bases de dados e a interação entre estes dois elementos. Desta forma, e atendendo às dificuldades identificadas por alguns autores neste tipo de aprendizagem, foi desenvolvido um conjunto de estratégias e atividades que culminaram num projeto final. Projeto esse que, no seu desenvolvimento foi dividido em cinco fases a concretizar e privilegiou a interdisciplinaridade, a autonomia, o sentido de responsabilidade e o trabalho colaborativo sob a orientação do professor.
Assim, tendo como suporte uma aprendizagem baseada em projetos (PjBL), pretende-se esclarecer em que medida a metodologia contribuiu para a consolidação de conceitos de programação de linguagens script em ambiente cliente-servidor.
De acordo com a caracterização feita da turma e com a ficha diagnóstica aplicada, foi possível ajustar as planificações elaboradas para um conjunto de nove aulas com duração de 90 minutos cada, com o intuito de motivar os alunos para conceitos nos quais evidenciam algumas dificuldades de aprendizagem, quer pela sua natureza científica como pelas suas implicações cognitivas.
Com o objetivo de avaliar o produto desenvolvido pelos alunos, bem como o seu processo, foram aplicadas grelhas de observação de aula e de avaliação das fases do projeto. Para além disso, foram aplicados outros instrumentos de avaliação referentes à metodologia utilizada bem como ao decurso da intervenção.This report, completed within the curricular unit of Intro to Professional Practices IV of the Masters Degree in Informatics Teaching, at the University of Lisbon, refers to the description of the experience of supervised teaching at the D. Dinis High school.
The intervention was carried out with a 12th grade class of the Informatics Systems Management and Programming Professional Technical Training Course, in the subject of Programming and Information Systems, more specifically in the optional module of Web Pages Design Tools. The class is made up of 15 male students and only 2 female students.
Taking into consideration the objectives set for the above mentioned module, the concepts approached were programming language (script), database management systems and the interaction between the two elements. This way, and considering the difficulties identified by some authors in this type of learning, a set of strategies and activities were developed which culminated in a final project. This project was eventually divided into five stages to be completed, privileging the interdisciplinary, a sense of autonomy, responsibility and collaborative work under the teacher’s guidance.
Thus, by supporting itself on a project-based type of learning (PjBL), one intends to clarify how this methodology has contributed to cement the concepts of scripting language in a client-server environment.
According to the characterization of the class and the diagnostic chart applied, it was possible to adjust the plans designed to a set of nine 90-minute-long classes, with the purpose of motivating students to learn the concepts in which they had showed some learning difficulties, whether due to its scientific nature or cognitive implications.
Aiming at evaluating the students learning process, this study applied class observation tables and project stage evaluations. Furthermore, other evaluation instruments were applied related with the methodology used as well as with the development of the intervention
Dematerialization of information management processes
No full textTrabalho de projecto de mestrado, Engenharia Informática (Arquitectura, Sistemas e Redes de Computadores), Universidade de Lisboa, Faculdade de Ciências, 2014Com o objectivo de expandir a diversidade de opções para os seus clientes, a Novabase tem interesse em explorar alternativas open source na área de enterprise search (ES), enterprise content management (ECM) e business process management (BPM). ES é um motor de busca composto por dois componentes, sendo o mais importante a pesquisa num índice invertido. Os candidatos são o Search Daimon [70], Solr [72] e ElasticSearch [21]. O Search Daimon é uma solução já muito completa, com muitas funcionalidades já feitas mas, não foi possível encontrar um manual ou o quer que seja que ajudasse a navegar e a modificar o código fonte e no excerto que vi, não estava comentado e foi difícil de ler. Uma alternativa de pesquisa open-source é o Lucene. O Lucene [51] é um motor de busca open source de muito elevada eficiência que trabalha sobre um índice invertido. É actualmente mantido pela Apache. O Solr [72] ´e um sistema que altera, melhora e diversifica a interface do Lucene permitindo usar o Lucene com um API REST e um conjunto de funcionalidades de alto nível. O Solr é desenvolvido pela Apache no qual, recentemente, foi lançada a funcionalidade de trabalhar em cloud. O ElasticSearch é um search engine que altera, melhora e diversifica a interface do Lucene permitindo usar o Lucene com um API REST. O Search daimon [70], pouco chega a ser considerado por causa da falta de informação sobre como trabalhar com ele sem ser com a interface gráfica. O Solr tem um manual muito completo [73], bem como o ElasticSearch [27]. As versões mais recentes do Solr permitem funcionar em cloud, o mesmo para o ElasticSearch. Aliás, o ElasticSearch sempre foi pensado para funcionar em cloud ao contrário do Solr que foi adaptado para funcionar em cloud. O ElasticSearch permite alterar muitas das suas opções incluindo adicionar e remover nós do swarm sem ser necessário reiniciar o servidor [28]. O Solr necessita de reiniciar sempre que existe uma alteração a fazer. Para pesquisa, o Solr só funciona usando uma query string. O ElasticSearch funciona com uma query string e também funciona com um objecto JavaScript Object Notation (JSON) bem estruturado [27]. O Solr usa JSON, Extensible Markup Language (XML) e comma-separated values (CSV) para alterar opções e para gravar dados. Destes dois, o ElasticSearch foi escolhido como sendo o melhor. Na parte de Enterprise content management (ECM), foram escolhidas as plataformas Nuxeo [55] e Alfresco [4]. Como critério, é necessário que os ECM tenham todas as versões open source. O Alfresco tem uma versão que necessita de uma licença paga mas o seu código é open source. O Nuxeo tem a versão completa, que permite usar o potencial todo do programa, disponível livre de custos. Sem contar com as interfaces como o utilizador (GUI) de que o utilizador tem acesso, ambos oferecem as mesmas funcionalidades com muito pequenas diferenças (ver quadros na sub-seccão “Comparing solutions” do 2.2.2). Embora o Alfresco community e o Nuxeo sejam muito parecidos, o Nuxeo desenvolveu uma ferramenta online paga, Nuxeo studio, que faz o mesmo que o Alfresco Enterprise. O Nuxeo studio [61] ´e um conjunto de ferramentas que oferecem um GUI [62] para controlar quase tudo no Nuxeo. Por causa da grande quantidade de semelhanças entre os dois e como os projectos em que ECM pode ser usado, torna-se impossível escolher qual dos dois é a melhor opção para o maior número de projectos. Mesmo assim, tendo em conta os vários parâmetros e caracteristicas do Nuxeo que estudei vs o equivalente do Alfresco e vice versa e com a nova vers˜ao do Nuxeo, concluo que o Nuxeo, embora não seja uma escolha ideal, é um ECM melhor pelas funcionalidades que tem, facilidade de personalização e pela organização e simplicidade. O ECM escolhido foi o Alfresco porque, independentemente que o Nuxeo seja melhor, se não for suficientemente conhecido, é o mesmo que não existir, independentemente do quão bom ele seja e estável, sem erros. O BPM decidido foi o que estava previsto na proposta inicial. Tendo já estes dados todos prontos, foi-me dada a tarefa de desenvolver um programa para integrar o ECM escolhido (Alfresco) com o BPM escolhido (jBPM). Durante a análise do jBPM, a empresa introduziu-me o Activiti como uma alternativa a ter a conta. Por estar a não usar um framework no primeiro projecto, um segundo projecto, baseado no primeiro, foi iniciado para executar o mesmo que o antecessor. Este projecto foi desenvolvido usando o primefaces e tinha, como um dos objectivos, comparar o Activiti e o jBPM. Com o prazo a acabar e por falta de informac¸ ˜ao dos superiores, este foi abandonado incompleto e o promeiro projecto foi retomado. No final, o primeiro projecto ficou uma prova de conceito para demonstrar uma possível interface muito versátil e muito personalizável que usa o Activiti (faltam algumas funcionalidades) ou o jBPM (suporte completo) como fonte para BPM e uma ligação CMIS para uma ligação ECM usando os dois para trabalho em equipa para desenvolver tarefas humanas.Enterprise content management (ECM) [77] appeared some years ago with the main purpose to reduce the amount of time dedicated to deal with the paperwork required to run a business. Assets were (and still are, for most companies) stored in large warehouses with strict sorting and very strict access rights. Without an ECM, when an employee requires a specific document, he would have to ask someone to search the document, get the document, and deliver the document to him, potentially, in a different building. Having an employee whose main purpose is to search and deliver company’s assets to whom requires them is probably not the most productive way of using an employee’s time. The ECM’s main work is to place a mirror to that repository and those employees who would run around delivering the documents (or copies of them) and manage the assets as if it was physical paper documents, except everything is digital while doing many other asset related tasks in the background. The usual setup is having an ECM working along an enterprise search backend and, optionally, a business process management (BPM) [15]. The enterprise search backend is responsible for indexing all search relevant information that exists in the ECM so that everything can be easily found with the known information about the thing. The BPM takes care of many internal system communications with the workflow management as its main feature
Aprendizagem baseada em projetos na consolidação de conceitos de programação de linguagens SCRIPT
No full textRelatório da prática de ensino supervisionada, Mestrado em Ensino de Informática, Universidade de Lisboa, 2014O presente relatório, elaborado no âmbito da unidade curricular de Introdução à Prática Profissional IV do Mestrado em Ensino de Informática da Universidade de Lisboa, refere-se à descrição da experiência da prática de ensino supervisionada realizada na Escola Secundária D. Dinis.
A intervenção foi realizada com uma turma do 12.ºAno do Curso Profissional Técnico de Gestão e Programação de Sistemas Informáticos, na disciplina de Programação e Sistemas de Informação, mais especificamente no módulo opcional de Ferramentas de Desenvolvimento de Páginas Web. Esta turma é constituída por 15 alunos do sexo masculino e apenas dois do sexo feminino.
Tendo como referência os objetivos estabelecidos para o referido módulo, foram abordados conceitos de linguagem de programação script, sistemas de gestão de bases de dados e a interação entre estes dois elementos. Desta forma, e atendendo às dificuldades identificadas por alguns autores neste tipo de aprendizagem, foi desenvolvido um conjunto de estratégias e atividades que culminaram num projeto final. Projeto esse que, no seu desenvolvimento foi dividido em cinco fases a concretizar e privilegiou a interdisciplinaridade, a autonomia, o sentido de responsabilidade e o trabalho colaborativo sob a orientação do professor.
Assim, tendo como suporte uma aprendizagem baseada em projetos (PjBL), pretende-se esclarecer em que medida a metodologia contribuiu para a consolidação de conceitos de programação de linguagens script em ambiente cliente-servidor.
De acordo com a caracterização feita da turma e com a ficha diagnóstica aplicada, foi possível ajustar as planificações elaboradas para um conjunto de nove aulas com duração de 90 minutos cada, com o intuito de motivar os alunos para conceitos nos quais evidenciam algumas dificuldades de aprendizagem, quer pela sua natureza científica como pelas suas implicações cognitivas.
Com o objetivo de avaliar o produto desenvolvido pelos alunos, bem como o seu processo, foram aplicadas grelhas de observação de aula e de avaliação das fases do projeto. Para além disso, foram aplicados outros instrumentos de avaliação referentes à metodologia utilizada bem como ao decurso da intervenção.This report, completed within the curricular unit of Intro to Professional Practices IV of the Masters Degree in Informatics Teaching, at the University of Lisbon, refers to the description of the experience of supervised teaching at the D. Dinis High school.
The intervention was carried out with a 12th grade class of the Informatics Systems Management and Programming Professional Technical Training Course, in the subject of Programming and Information Systems, more specifically in the optional module of Web Pages Design Tools. The class is made up of 15 male students and only 2 female students.
Taking into consideration the objectives set for the above mentioned module, the concepts approached were programming language (script), database management systems and the interaction between the two elements. This way, and considering the difficulties identified by some authors in this type of learning, a set of strategies and activities were developed which culminated in a final project. This project was eventually divided into five stages to be completed, privileging the interdisciplinary, a sense of autonomy, responsibility and collaborative work under the teacher’s guidance.
Thus, by supporting itself on a project-based type of learning (PjBL), one intends to clarify how this methodology has contributed to cement the concepts of scripting language in a client-server environment.
According to the characterization of the class and the diagnostic chart applied, it was possible to adjust the plans designed to a set of nine 90-minute-long classes, with the purpose of motivating students to learn the concepts in which they had showed some learning difficulties, whether due to its scientific nature or cognitive implications.
Aiming at evaluating the students learning process, this study applied class observation tables and project stage evaluations. Furthermore, other evaluation instruments were applied related with the methodology used as well as with the development of the intervention
- …
