Luis Soares Barbosa

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.

How learning occurs within Free/Libre Open Source (FLOSS) communities and what is the dynamics 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.

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. In a series of papers this process has been detailed and taken as a basis for a specification methodology for reconfigurable systems. The present paper extends this work by showing how a proof calculus (in both a Hilbert and a tableau based format) for the hybridised version of a logic can be systematically generated from a proof calculus for the latter. Such developments provide the basis for a complete proof theory for hybrid(ised) logics, and thus pave the way to the development of (dedicated) proof support. Decidability results for hybrid(ised) logics.Generation of Hilbert calculi for hybrid(ised) logics.Generation of Tableau systems for hybrid(ised) logics.

n/a

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 D↓-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.

Background: A software system is self-adaptive when it is able to dynamically and autonomously respond to changes detected either in its internal components or in its deployment environment. This response is expected to ensure the continuous availability of the system by maintaining its functional and non-functional requirements.

Methods: Since these systems are usually distributed, coordination middleware (typically a centralised architectural entity) plays a definitive role in establishing the system goals. For these reasons, adaptations may be triggered at coordination level, issuing reconfigurations to such a coordination entity. However, predicting when exactly reconfigurations are needed, and if they will lead the system into a non disruptive configuration, is still an issue at this level. This paper builds on a framework for formal verification of architectural requirements, either from a qualitative or quantitative (probabilistic) point of view, which will leverage analysis and adaptation prediction.

Results: In order to address the mentioned difficulties, it is discussed both a model that lays down reconfiguration strategies, planned at design time, and a process that actively uses such a model to trigger coordination-targeted reconfigurations at run time. Moreover, a cloud-based architecture for the implementation of this strategy is proposed, as an attempt to deliver adaptation as a service. A case study is presented that assesses the suitability of the approach for real-world software systems.

Conclusions: We highlight the use of formal models to represent the coordination layer and necessary reconfigurations of a software system, and also to predict the need for (and to trigger) adaptations.

Software reconfigurability became increasingly relevant to the architectural process due to the crescent dependency of modern societies on reliable and adaptable systems. Such systems are supposed to adapt themselves to surrounding environmental changes with minimal service disruption, if any. This paper introduces an engine that statically applies reconfigurations to (formal) models of software architectures. Reconfigurations are specified using a domain specific language— ReCooPLa—which targets the manipulation of software coordination structures, typically used in service-oriented architectures (soa). The engine is responsible for the compilation of ReCooPLa instances and their application to the relevant coordination structures. The resulting configurations are amenable to formal analysis of qualitative and quantitative (probabilistic) properties.