Suchergebnisse

On the eve of accession to the European Union, Malta like all new members states, experienced considerable pressure for change. This included a drive to adapt RTDI policies for participation in the European Research Area. For a small transition economy with limited resources there was a need to adopt a creative approach to policy development. In the period 2002-2003 foresight was introduced to Malta via three pilot projects conducted by the MCST. These pilot projects played an important role in breaking path-dependencies. They liberated the mind-sets of stakeholders and provided occasion for mutual learning on systemic issues. Foresight is now an inte- gral part of the day-to-day work of the MCST which continues to promote and encourage its application to other policy domains. ; N/A

The research work disclosed in this publication is partially funded by the Strategic Educational Pathways Scholarship Scheme (Malta). The scholarship is part financed by the European Union European Social Fund. ; The use of behavioural contracts, to specify, regulate and verify systems, is particularly relevant to runtime monitoring of distributed systems. System distribution poses major challenges to contract monitoring, from monitoring-induced information leaks to computation load balancing, communication overheads and fault-tolerance. We present mDPi, a location-aware process calculus, for reasoning about monitoring of distributed systems. We define a family of Labelled Transition Systems for this calculus, which allow formal reasoning about di erent monitoring strategies at di erent levels of abstractions. We also illustrate the expressivity of the calculus by showing how contracts in a simple contract language can be synthesised into di erent mDPi monitors. ; peer-reviewed

Given the strict legal frameworks which regulate the movements and management of funds, building financial applications typically proves to be prohibitively expensive for small companies. Not only is it the case that understanding legal requirements and building a framework of compliance checks to ensure that such legislation is adhered to is a complex process, but also, service providers such as banks require certification and reporting before they are willing to take on the risks associated with the adoption of applications from small application developers. In this paper, we propose a solution which provides a centralised Open Payments Ecosystem which supports compliance checking and allows for the matching of financial applications with service providers and programme managers, automatically providing risk analysis and reporting. The solution proposed combines static and dynamic verification in a real-life use case, which can shed new insights on the use of formal methods on large complex systems. We also report on the software engineering challenges encountered when analysing formal requirements arising from the needs of compliance to applicable legislation. ; peer-reviewed

As with all fields of application, policy-making can frequently fall into the trap of not questioning whether the regular, oft-used solutions are the only way to solve a new problem. Far too frequently, it happens that, not only is a particular policy instrument not the best answer, but it is not even a valid answer to the problem in the first place! Systematic approaches to policy formulation, such as foresight, may appear at the outset as presenting a toolkit of routinised methodologies to be followed religiously by the newly initiated. Yet foresight practice itself shows that not only do foresight experiences generated in one country or region defy close emulation, but that foresight as a phenomenon is undergoing constant change in response to the evolving socio-economic context. ; peer-reviewed

This research has received funding from the European Union's Horizon 2020 research and innovation programme under grant number 666363. ; Where full static analysis of systems fails to scale up due to system size, dynamic monitoring has been increasingly used to ensure system correctness. The downside is, however, runtime overheads which are induced by the additional monitoring code instrumented. To address this issue, various approaches have been proposed in the literature to use static analysis in order to reduce monitoring overhead. In this paper we generalise existing work which uses control-flow static analysis to optimise properties specified as automata, and prove how similar analysis can be applied to more expressive symbolic automata - enabling reduction of monitoring instrumentation in the system, and also monitoring logic. We also present empirical evidence of the effectiveness of this approach through an analysis of the effect of monitoring overheads in a financial transaction system. ; peer-reviewed