Search

Reinforcement Learning is at the core of a recent revolution in Arti cial Intelligence. Simultaneously, we are witnessing the emergence of a new eld: Quantum Machine Learning. In the context of these two major developments, this work addresses the interplay between Quantum Computing and Reinforcement Learning. Learning by interaction is possible in the quantum setting using the concept of oraculization of environments. The paper extends previous oracular instances to address more general stochastic environments. In this setting, we developed a novel quantum algorithm for near-optimal decision-making based on the Reinforcement Learning paradigm known as Sparse Sampling. The proposed algorithm exhibits a quadratic speedup compared to its classical counterpart. To the best of the authors' knowledge, this is the first quantum planning algorithm exhibiting a time complexity independent of the number of states of the environment, which makes it suitable for large state space environments, where planning is otherwise intractable., This work is financed by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project UIDB/50014/2020.

This extended abstract reports on on-going research on quantum algorithmic approaches to the problem of generalised tree search that may exhibit effective quantum speedup, even in the presence of non-constant branching factors. Two strategies are briefly summarised and current work outlined.

A national census is an official count of a country's population that aims to motivate and measure sustainable development. Traditionally, a census is a cumbersome manual operation that involves distributing surveys to all households in the country through field agents or by mail. Recently, some countries have utilized voluntary electronic submissions in addition to the manual work to reduce costs and increase efficiency. However, an increasing number of countries are resorting to a register-based census that uses pre-existing official registers to derive its data. This paper describes Oman's upcoming register-based census, e-Census 2020, and analyses it against the European Commission's necessary conditions that facilitate a successful transition from a traditional to a register-based census [1].

The development of smart mobility initiatives requires specialized and contextualized policies addressing the needs and interests of many stakeholders involved. Since the development of such policies is challenging, there is a need to learn from the experience of many cities around the world offering efficient and successfully adopted smart mobility services. However, in practice, the information provided about such initiatives is shallow and unstructured. To address this issue, we study the state of the art in mobility services, reviewing scientific publications and 42 smart mobility services delivered by nine smart cities around the world, and we propose a taxonomy for planning and designing smart mobility services. The taxonomy provides a common vocabulary to discuss and share information about such services. It comprises eight dimensions: type of services, maturity level, users, applied technologies, delivery channels, benefits, beneficiaries, and common functionality. The contribution of the proposed taxonomy is to serve as a tool for guiding policy makers by identifying a spectrum of mobility services that can be provided, to whom, what technologies can be used to deliver them, and what is the delivered public value so to justify their implementation. In addition, the taxonomy can also assist researchers in further developing the domain. By identifying common functionality, it could also help Information Technology (IT) teams in building and maintaining smart mobility services. Finally, we further discuss usage scenarios of the taxonomy by policy makers, IT staff and researchers., NORTE-01-0145-FEDER-000037, supported by Norte Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement, through the European Regional Development Fund (EFDR). The first author is also supported by the Portuguese funding agency, FCT, under grant PD/BD/52238/2013

Photosynthesis is an important and complex physical process in nature, whose comprehensive understanding would have many relevant industrial applications, for instance in the field of energy production. In this paper we propose a quantum algorithm for the simulation of the excitonic transport of energy, occurring in the first stage of the process of photosynthesis. The algorithm takes in account the quantum and environmental effects (pure-dephasing), influencing the quantum transport. We performed quantum simulations of such phenomena, for a proof of concept scenario, in an actual quantum computer the IBM Q, of 5 qubits. We validate the results with the Haken-Str\"obl model and discuss the influence of environmental parameters on the efficiency of the energy transport., POCI-01-0145-FEDER-030947

Although Finite-State Automata (FSA) have been successfully used in modeling and control of Discrete Event Systems (DESs), they are limited to represent complex and advanced features of DESs, such as context recognition and switching. The literature has suggested that a FSA can nevertheless be enriched with parameters properly collected from the modeled system, so that this favors design and control. A parameter can be embedded either on transitions or states. However, each approach is structured within a specific framework, so that their comparison and integration are not straightforward and they may lead to different control solutions, modeled, computed and implemented using distinct strategies. In this paper, we show how to combine advantages from parameters in modeling and control of DESs. Each approach is structured and their advantages are identified and exemplified. Then, we propose a conversion method that allows to translate a design-friendly model into a synthesis-efficient structure. Examples illustrate the approach., CNPq, under grant number 402145/2016-0, 09, Araucaria Foundation, CAPES, and FINEP, and partially supported by ERDF - The European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme, and by National Funds through FCT - Fundação para a Ciência e a Tecnologia, within project POCI- ˆ 01-0145-FEDER-030947 (KLEE)

In the context of digital transformation by governments, the public sector and other organizations, many information is moving to digital platforms. Chatbots and similar question-answering systems are becoming popular to answer information queries, opposed to browsing online repositories or webpages. State-of-the-art approaches for these systems may be laborious to implement, hard to train and maintain, and also require a high level of expertise. This work explores the definition of a generic framework to systematically build question-answering systems. A sandbox implementation of this framework enables the deployment of turnkey systems, directly from already existing collections of documents. These systems can then be used to provide a question-answering system communication channel to enrich the organization digital presence.

Applications developed over the cloud coordinate several, often anonymous, computational resources, distributed over different execution nodes, within flexible architectures. Coordination models able to represent quantitative data provide a powerful basis for their analysis and validation. This paper extends IMCreo, a semantic model for Stochastic reo based on interactive Markov chains, to enhance its scalability, by regarding each channel and node, as well as interface components, as independent stochastic processes that may (or may not) synchronise with the rest of the coordination circuit., Comment: In Proceedings iFMCloud 2016, arXiv:1610.07700

Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms. This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting., In Proceedings Refine'15, arXiv:1606.01344

ERDF - The European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundacao para a Ciencia e a Tecnologia, within project POCI-01-0145-FEDER-030947. and project with reference UID/MAT/04106/2019 at CIDMA. D. Figueiredo also acknowledges the support given by FCT via the PhD scholarship PD/BD/114186/2016

Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter. published

The e-Oman Integration Platform is a data hub that enables data exchanges across government in response to transactions. With millions of transactions weekly, and thereby data exchanges, we propose to investigate the potential of gathering intelligence from these linked sources to help government officials make more informed decisions. A key feature of this data is the richness and accuracy, which increases the value of the learning outcome when augmented by other big and open data sources. We consider a high-level framework within a government context, taking into account issues related to the definition of public policies, data privacy, and the potential benefits to society. A preliminary, qualitative validation of the framework in the context of e-Oman is presented. This paper lays out foundational work into an ongoing research to implement government decision-making based on big data.

Regulations, laws, norms, and other documents of legal nature are a relevant part of any governmental organisation. During digitisation and transformation stages towards a digital government model, information and communication technologies are explored to improve internal processes and working practices of government infrastructures. This paper introduces preliminary results on a research line devoted to developing visualisation techniques for enhancing the readability and comprehension of legal texts. The content of documents is conveyed to a well-defined model, which is enriched with semantic information extracted automatically. Then, a set of digital views are created for document exploration from both a structural and semantic point of view. Effective and easier to use digital interfaces can enable and promote citizens engagement in decision-making processes, provide information for the public, and also enhance the study and analysis of legal texts by lawmakers, legal practitioners, and assorted scholars.

The structure of a reactive transition system can to be modi ed on the y by e.g. removing, reversing or adding new transitions. The topic has been studied by D. Gabbay and his collaborators in di erent contexts. In this paper we take their work a step further, introducing a suitable notion of bisimulation and obtaining a Hennessy-Milner theorem with respect to a hybrid logic in which transition properties can be expressed. Our motivation is to provide a characterisation of equivalence for such systems in order to exploit their possible roles in the formal description of software connectors in Reo, either from a behavioural (semantic) or spatial (syntactic) point of view., “SmartEGOV/NORTE-01-0145-FEDER-000037”, supported by Norte Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement, through the European Regional Development Fund (EFDR). Additional support was provided by the European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project UID/MAT/04106/2013 at CIDMA. The first author is also supported by an Individual Doctoral Grant (reference number PD/BD/114186/2016)

This note revisits layered logics from a coalgebraic point of view, and proposes a naturality condition to express the typical hierarchical requirement under which all abstract transitions should be traceable in more specialised layers.

Burden reduction is a key issue in modern public administrations' and businesses' agendas. Compliance with mandatory regulations can have a direct impact on a country's economic performance, growth, and development. Research in this area, contributes to a better understanding of the implications and context of administrative burden, and increases the efficiency of the strategies adopted to reduce it. The goal of this study is to undertake a review of the current state of the art on Administrative Burden Reduction (ABR), in order to gain a deeper insight about the subject, identify current gaps, and better plan for future research. A total of 122 papers were identified as relevant, out of a pool of 742 papers retrieved from the current literature. The relevant papers were analyzed across four dimensions: methodology, type and focus, and targeted stakeholders. Three key gaps were identified and discussed in relation to: citizen orientated services and burden reduction; empirical research and post-initiative re-evaluation; and, the role of stakeholders, interest groups and end-users in driving ABR. Lastly a conceptual framework model and next steps are proposed.

In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper’s main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics., Fundação para a Ciência e a Tecnologia (FCT)

The complexity of modern software systems entails the need for reconfiguration mechanisms gov- erning the dynamic evolution of their execution configurations in response to both external stimulus or internal performance measures. Formally, such systems may be represented by transition systems whose nodes correspond to the different configurations they may assume. Therefore, each node is en- dowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of this sort of systems. Therefore, the quest for suitable notions of equivalence and refinement between models of hybrid logic specifications becomes fundamental to any design discipline adopting this perspective. This paper contributes to this effort from a distinctive point of view: instead of focussing on a specific hybrid logic, the paper introduces notions of bisimilarity and refinement for hybridised logics, i.e. standard specification logics (e.g. propositional, equational, fuzzy, etc) to which modal and hybrid features were added in a systematic way., Comment: In Proceedings Refine 2013, arXiv:1305.5634

Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain.

SmartEGOV: Harnessing EGOV for Smart Governance (Foundations, methods, Tools) / NORTE-01-0145-FEDER000037, supported by Norte Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement, through the European Regional Development Fund (EFDR

Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional.

The orchestration of high performance computing (HPC) services to build scientific applications is based on complex workflows. A challenging task consists of improving the reliability of such workflows, avoiding faulty behaviors that can lead to bad consequences in practice. This paper introduces a certifier component for certifying scientific workflows in a certification framework proposed for HPC Shelf, a cloud-based platform for HPC in which different kinds of users can design, deploy and execute scientific applications. This component is able to inspect the workflow description of a parallel computing system of HPC Shelf and check its consistency with respect to a number of safety and liveness properties specified by application designers and component developers.

Asymmetric combination of logics is a formal process that develops the characteristic features of a specific logic on top of another one. Typical examples include the development of temporal, hybrid, and probabilistic dimensions over a given base logic. These examples are surveyed in the paper under a particular perspective—that this sort of combination of logics possesses a functorial nature. Such a view gives rise to several interesting questions. They range from the problem of combining translations (between logics), to that of ensuring property preservation along the process, and the way different asymmetric combinations can be related through appropriate natural transformations.

Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete actions guarded by Boolean tests.

This paper sums up the Portuguese experience on launching and implementing a number of successful EGOV policies at different levels. Such a success was based on a holistic understanding of EGOV, in the confluence of technology, administrative reform and innovation processes, and enforced through a number of well-defined, consistent policies carried out over time. The role of national agencies, independent from local political instances and private interests, in the implementation of an effective EGOV strategy is also stressed.

By 2050 it is expected that 66% of the world population will reside in cities, compared to 54% in 2014. One particular challenge associated to urban population growth refers to transportation systems, and as an approach to face it, governments are investing significant efforts enhancing public transport services. An important aspect of public transport is ensuring that licensing of such services fulfill existing government regulations. Due to the differences in government regulations, and to the difficulties in ensuring the fulfillment of their specific features, many local governments develop tailored Information and Communication Technology (ICT) solutions to automate the licensing of public transport services. In this paper we propose an ontology for licensing such services following the REFSENO methodology. In particular, the ontology captures common concepts involved in the application and processing stage of licensing public bus passenger services. The main contribution of the proposed ontology is to define a common vocabulary to share knowledge between domain experts and software engineers, and to support the definition of a software product line for families of public transport licensing services.

Administrative burden represents the costs to businesses, citizens and the administration itself of complying with government regulations and procedures. The burden tends to increase with new forms of public governance that rely less on direct decisions and actions undertaken by traditional government bureaucracies, and more on government creating and regulating the environment for other, non-state actors to jointly address public needs. Based on the reviews of research and policy literature, this paper explores administrative burden as a policy problem, presents how Digital Government (DG) could be applied to address this problem, and identifies societal adoption, organizational readiness and other conditions under which DG can be an effective tool for Administrative Burden Reduction (ABR). Finally, the paper tracks ABR to the latest Contextualization stage in the DG evolution, and discusses possible development approaches and technological potential of pursuing ABR through DG.

The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of pi-institutions. This leads to a smooth generalization of the refinement-by-interpretation approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a refinement calculus of structured specifications in and across arbitrary pi-institutions., Comment: In Proceedings Refine 2011, arXiv:1106.3488

Current software development often relies on non trivial coordination logic for combining autonomous services, eventually running on different platforms. As a rule, however, such a coordination layer is strongly weaved within the application at source code level. Therefore, its precise identification becomes a major methodological (and technical) problem and a challenge to any program understanding or refactoring process. The approach introduced in this paper resorts to slicing techniques to extract coordination data from source code. Such data is captured in a specific dependency graph structure from which a coordination model can be recovered either in the form of an Orc specification or as a collection of code fragments corresponding to the identification of typical coordination patterns in the system. Tool support is also discussed., Fundação para a Ciência e a Tecnologia (FCT) - projeto Mondrian, PTDC/EIA-CCO/108302/2008

Research in formal methods emphasizes a funda- mental interconnection between modeling, calculation and prototyping, made possible by a common unambiguous, mathematical semantics. This paper, building on a broader research agenda on coalgebraic semantics for Unified Modeling Language diagrams, concentrates on class diagrams and discusses how such a coalgebraic perspective can be of use not only for formalizing their specification, but also as a basis for prototyping., This research was partially supported by a grant from the GLANCE funding program of NWO, through project CooPer (600.643.000.05N12), aswell as by Fct (the Portuguese Foundation for Science and Technology) under contract PTDC/EIA/73252/2006.

A transition system can be presented either as a binary relation or as a coalgebra for the powerset functor, each representation being obtained from the other by transposition. More generally, a coalgebra for a functor F generalises transition systems in the sense that a shape for transitions is determined by F, typically encoding a signature of methods and observers. This paper explores such a duality to frame in purely relational terms coalgebraic refinement, showing that relational (data) refinement of transition relations, in its two variants, downward and upward (functional) simulations, is equivalent to coalgebraic refinement based on backward and forward morphisms, respectively. Going deeper, it is also shown that downward simulation provides a complete relational rule to prove coalgebraic refinement. With such a single rule the paper defines a pre-ordered calculus for refinement of coalgebras, with bisimilarity as the induced equivalence. The calculus is monotonic with respect to the main relational operators and arbitrary relator F, therefore providing a framework for structural reasoning about refinement.

This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call \(\mathcal {D}^{\downarrow }\)-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.

Able to simultaneously encode discrete transitions and continuous behaviour, hybrid automata are the de facto framework for the formal specification and analysis of hybrid systems. The current paper revisits hybrid automata from a coalgebraic point of view. This allows to interpret them as state-based components, and provides a uniform theory to address variability in their definition, as well as the corresponding notions of behaviour, bisimulation, and observational semantics.

How learning occurs within Free/Libre Open Source (FLOSS) communities and what is the dynamics of such projects (e.g. the life cycle of such projects) are very relevant questions when considering the use of FLOSS projects in a formal education setting. This paper introduces an approach based on the 3C collaboration model (communication, coordination and cooperation) to represent the collaborative learning dynamics within FLOSS communities. To explore the collaborative learning potential of FLOSS communities a number of questionnaires and interviews to selected FLOSS contributors were run. From this study a 3C collaborative model applicable to FLOSS communities was designed and discussed.

The quest for sound foundations for the orchestration of web services is still open. To a great extent its relevance comes from the possibility of defining formal semantics for new language standards (like BPEL4WS or WS-CDL) in this emerging and challenging technology. As a step in that direction, this paper resorts to a notion of configuration, developed by the authors in the context of a Reo-like exogenous coordination model for software components, to formally express service orchestration. The latter is regarded as involving both the architectural assembly of independent services and the description of their interactions., Fundação para a Ciência e a Tecnologia (FCT) - PURe Project, contract POSI/ICHS/44304/2002.

A partial component is a process which fails or dies at some stage, thus exhibiting a finite, more ephemeral behaviour than expected (eg, operating system crash). Partiality --- which is the rule rather than exception in formal modelling --- can be treated mathematically via totalization techniques. In the case of partial functions, totalization involves error values and exceptions. In the context of a coalgebraic approach to component semantics, this paper argues that the behavioural counterpart to such functional techniques should extend behaviour with try-again cycles preventing from component collapse, thus extending totalization or transposition from the algebraic to the coalgebraic context. We show that a refinement relationship holds between original and totalized components which is reasoned about in a coalgebraic approach to component refinement expressed in the pointfree binary relation calculus. As part of the pragmatic aims of this research, we also address the factorization of every such totalized coalgebra into two coalgebraic components --- the original one and an added front-end --- which cooperate in a client-serverstyle., Fundação para a Ciência e a Tecnologia (FCT) - PURe Project under contract POSI/ICHS/44304/2002.

This paper characterises refinement of state-based software components modelled as pointed coalgebras for some Set endofunctors. The proposed characterisation is parametric on a specification of the underlying behaviour model introduced as a strong monad. This provides a basis to reason about (and transform) state-based software designs. In particular, it is shown how refinement can be applied to the development of the inequational subset of a calculus of generic software components.

ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems in terms of architectural patterns. The language supports the specification of architectures and their reconfiguration. This paper introduces a language extension for precisely describing the structural design decisions that pattern instances must respect in their (re)configurations. The extension is a propositional modal logic with recursion and nominals referencing components, i.e., a hybrid µ-calculus. Its expressiveness allows specifying safety and liveness constraints, as well as paths and cycles over structures. Refinements of classic architectural patterns are specified.

Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smell-free using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.

This paper introduces HHL, a hierarchical variant of hybrid logic. First-order correspondence and a Hennessy-Milner like theorem relating (hierarchical) bisimulation and logical equivalence for HHLare presented. Combining hierarchical transition structures with the ability to refer to specific states at any level of description, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science., Dynamic logic combines logic with programs, which at a certain level of abstraction, can be regarded as behaviours changing the system state and, therefore, the truth value of formulas. This paper suggests a method for generating such logics for the domain of robot controllers and illustrates it with a logic for handling resource consumption.

Self-adaptive software systems are known to respond at run time to changes detected internally or in their environment, in an attempt to keep meeting their own functional requirements and agreed levels of service. Such response usually targets their architectures and involve, in particular, the possibility of their dynamic reconfiguration. In contexts where change is the rule rather than the exception, it is difficult to predict when exactly such reconfigurations are needed, and if they will lead the system into a suitable configuration. However, knowing the main attributes of the context, it is possible to plan configurations that will be more likely to perform well in some conjugation of values for such attributes. In this paper we discuss both a model that lays down reconfiguration strategies, planned at design time, and a strategy which actively uses such a model to trigger architectural adaptations at run time. This strategy builds on a framework intended to the formal verification of architectural requirements, either from a qualitative or quantitative (probabilistic) perspective.

As a complex artefact, software has to meet requirements formulated and verified at different levels of abstraction. A basic distinction is drawn between behavioural (dynamic) and data (static) aspects. From an educational point of view, although disguised under a number of different designations, both issues are usually present, but kept separated, in typical Computer Science undergraduate curricula. It is often argued that they tackle orthogonal problems through essentially different methods. This paper explores an alternative path in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

This paper is an attempt to apply the reasoning principles and calculational style underlying the so-called Bird-Meertens formalism to the design of process calculi, parametrized by a behaviour model. In particular, basically equational and pointfree proofs of process properties are given, relying on the universal characterisation of anamorphisms and therefore avoiding the explicit construction of bisimulations. The developed calculi can be directly implemented on a functional language supporting coinductive types, which provides a convenient way to prototype processes and assess alternative design decisions., (undefined)

It can be argued that participating in Free/Libre Open Source Software (FLOSS) projects can have a positive effect in the contributor's learning process. The need to collaborate with other contributors and to contribute to a project can motivate and implicitly foster learning. In order to validate such statements, it is necessary to (1) study the interactions between FLOSS projects' participants, and (2) explore the didactical value of participating in FLOSS projects, designing an appropriate questionnaire asking FLOSS contributors about their experience in FLOSS projects. In this paper, we illustrate how this questionnaire was designed and disseminated. We conclude the paper with results from 27 FLOSS projects contributors, determining that, not only they contribute and collaborate to the project and its community, but also that FLOSS contributors see that this type of activity can be regarded as a complement to formal education.

Argumentation and proof are two main ingredients in strategies for developing mathematical skills and structured reasoning. This paper reports on a research project aimed at 'refactoring' school Mathematics in other to achieve a higher degree of mathematical literacy. In a sense this builds on a number of 'lessons' learnt from the practice of Computing Science. We further argue that mathematical fluency, broadly understood as the ability to reason in terms of abstract models and the effective use of logical arguments and mathematical calculation, became a condition for democratic citizenship and sustainable development.

Publicado em "Integration of reusable systems". ISBN 978-3-319-04716-4, Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need for more sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic., (undefined)

This paper presents a comparative analysis of Free/Libre Open Source Software FLOSS Learning Management System LMS. Following a selection process we analyze the functionalities and characteristics of 8 tools commonly used in formal and informal education. More specifically we focus on the availability of different tools concerning communication and assistance, such as, forum, email, calendar, portfolios, etc. Our analysis showed that despite their similarities, the appropriateness of different FLOSS LMSs can be greatly affected by the specific needs of students, instructors and institutions.

Software connectors encapsulate interaction patterns between services in complex, distributed service-oriented applications. Such patterns evolve over time, in response to faults, changes in the expected QoS levels, emergent requirements or the reassessment of contextual conditions. This paper builds up on a model for connector reconfiguration to introduce notions of reconfiguration equivalence and refinement allowing for reasoning about them. This paves the way towards a (still missing) calculus of connector reconfigurations.