Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Category theory is proving a useful tool in programming and program specification - not only as a descriptive language but as directly applicable to programming and specification tasks. Category theory achieves a level of generality of description at which computation is still possible. We show that theorems from category theory often have constructive proofs in the sense that they may be encoded as programs. In particular we look at the computation of colimits in categories showing that general theorems give rise to routines which considerably simplify the rather awkward computation of colimits. The general routines arising from categorical constructions can be used to build programs in the 'combinatorial' style of programming. We show this with an example - a program to implement the semantics of a specification language. More importantly, the intimate relationship between these routines and algebraic specifications allows us to develop programs from certain forms of specifications. Later we turn to algebraic specifications themselves and look at properties of "monadic theories". We establish that, under suitable conditions: 1. Signatures and presentations may be defined for monadic theories and free theories on a signature may be constructed. 2. Theory morphisms give rise to ad junctions between categories of algebras and moreover a collection of algebras of a theory give rise to a new theory with certain properties. 3. Finite colimits and certain factorisations exist in categories of monadic theories. 4. Many-sorted, order-sorted and even category-sorted theories may be handled by somewhat extending the notion of monadic theories. These results show that monadic theories are sufficiently well-behaved to be used in the semantics of algebraic specification languages. Some of the constructions can be encoded as programs by the techniques mentioned above.

A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.

A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.

A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.

Smart contracts are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are among the most popular choices for smart contract development. However, there is a substantial gap in the knowledge of smart contracts between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. This thesis proposes a tool-supported method for translating Symboleo specifications into smart contracts. Its contributions include extensions to the existing Symboleo IDE, the implementation of the ontology and semantics of Symboleo into a reusable library, and the Symboleo2SC tool that generates Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. Experimentation with Symboleo2SC shows that legal contract specifications in Symboleo can be fully converted to smart contracts for monitoring purposes. Moreover, Symboleo2SC helps simplify the smart contract development process, saves development effort, and helps reduce risks of coding errors.

No description available.

Student mobility in the area of Higher Education (HE) is gaining more attention nowadays. It is one of the cornerstones of the Bologna Process being promoted at both national and international levels. However, currently there is no technical system that would support student mobility processes and assist users in authoring educational curricula involving student mobility. In this study, the problem of student mobility programmes generation based on existing modules and programmes is considered. A similar problem is being solved in an Intelligent Tutoring Systems field using Curriculum generation techniques, but the student mobility area has a set of characteristics limiting their application to the considered problem. One of main limiting factors is that mobility programmes should be developed in an environment with heterogeneous regulations. In this environment, various established routines and regulations are used to control different aspects of the educational process. These regulations can be different in different domains and are supported by different authors independently. In this thesis, a novel framework was developed for generation of student mobility programmes in an environment with heterogeneous regulations. Two core technologies that were coherently combined in the framework are hierarchical planning and policy-based management. The policy-based planner was designed as a central engine for the framework. It extends the functionality of existing planning technologies and provides the means to carry out planning in environments with heterogeneous regulations, specified as policies. The policy-based planner enforces the policies during the planning and guarantees that the resultant plan is conformant with all policies applicable to it. The policies can be supported by different authors independently. Using them, policy authors can specify additional constraints on the execution of planning actions and extend the pre-specified task networks. Policies are enforced during the planning in a coordinated manner: situations when a policy can be enforced are defined by its scope, and the outcomes of policy evaluation are processed according to the specially defined procedures. For solving the problem of student mobility programme generation using the policy-based planner, the planning environment describing the student mobility problem area was designed and this problem was formalised as a planning task. Educational processes valid throughout the HE environment were formalised using Hierarchical Task Network planning constructs. Different mobility schemas were encoded as decomposition methods that can be combined to construct complex mobility scenarios satisfying the user requirements. New mobility programmes are developed as detailed educational processes carried out when students study according to these programmes. This provides the means to model their execution in the planning environment and guarantee that all relevant requirements are checked. The postponed policy enforcement mechanism was developed as an extension of the policy-based planner in order to improve the planning performance. In this mechanism, future dead-ends can be detected earlier during the planning using partial policy requests. The partial policy requests and an algorithm for their evaluation were introduced to examine policies for planning actions that should be executed in the future course of planning. The postponed policy enforcement mechanism was applied to the mobility programme generation problem within the descending policy evaluation technique. This technique was designed to optimise the process of programme components selection. Using it, policies for different domains can be evaluated independently in a descending order, gradually limiting the scope for the required component selection. The prototype of student mobility programme generation solution was developed. Two case studies were used to examine the process of student mobility programmes development and to analyse the role of policies in this process. Additionally, four series of experiments were carried out to analyse performance gains of the descending policy evaluation technique in planning environments with different characteristics.

[pt] O desenvolvimento de conteúdos instrucionais utilizando as novas tecnologias de informação é um processo caro, demorado e complexo, que aponta para o estabelecimento de novas metodologias. É neste contexto que surge o conceito de Objeto de Aprendizagem (LO), cujo enfoque está em promover a reutilização do conteúdo. Entretanto, ao considerar o reuso de conteúdo, também se observa uma necessidade de seqüência - lo para formar conteúdos mais elaborados ou mais complexos. Nesta tese adota-se uma estratégia de representar LOs cada vez menores, representando separadamente conteúdo e prática, aqui denominados Objetos Componentes (OCs). Para a estruturação do conteúdo, adaptou-se uma proposta já existente e definiu-se um esquema conceitual adequado à representação de atividades (ou práticas) de aprendizagem. Com vista à composição dos OCs, foi igualmente definido um esquema conceitual envolvendo conteúdos e práticas. Assim, com base em um algoritmo de seqüenciamento de OCs, um professor pode compreender melhor a forma de implementar um objeto complexo, como uma aula ou um curso, reduzindo erros e eventuais omissões na implementação da solução. Este seqüenciamento deve seguir uma metodologia e deve ser especificado de modo não ambíguo. É neste contexto que também é apresentada uma linguagem para especificação de seqüências de objetos de aprendizagem, com uma sintaxe adequada à descrição das possíveis formas de seqüenciamento de LOs. Finalmente, descreve-se um estudo de caso ilustrando a utilização dos esquemas conceituais desenvolvidos, do algoritmo proposto e da linguagem de especificação de seqüências OCs. / [en] The development of instructional content using new Information Technologies is an expensive, time-consuming and complex process that leads to the development of new methodologies. It was in this context that the concept of Learning Objects (LOs) was proposed as an approach that promotes content reuse. However, if content is expressed as small LOs, it is also necessary to sequence them in order to build more elaborated and complex content. In this thesis we adopt a strategy to represent smaller LOs, modeling not only content but also practice, called Component Objects (COs) herein. In order to structure content we adapted an existing proposal and defined a conceptual schema to structure learning practices (or activities). We also defined a conceptual schema for composing these COs. Then, based on these conceptual schemas it was possible to propose an algorithm for sequencing COs, which supports a teacher/professor to better control the implementation of a complex content such as a class or a course, thus reducing errors and eventual omissions in its implementation. The sequencing process must follow a methodology and must be specified in a nonambiguous way. It is in this context that we also present a specification language for sequences of LOs, with a syntax that is adequate to the description of the possible ways of sequencing LOs. Finally, we describe a case study that shows the conceptual schemas that were proposed and the use of the sequencing algorithm and the specification language.