Abstract

Abstract
Financial institutions, acting as financial intermediaries, need to handle numerous information sources and feed them to multiple processing, storage, and display services. This requires filtering and routing, but these feeds are usually provided in custom formats and protocols that are not the best fit for further processing. Moreover, the sheer volume of information and stringent timeliness and reliability requirements make this a substantial task. In this paper, i) we characterize one of these information feeds (the Exchange Data Publisher feed from the NYSE Euronext European Cash Markets) and ii) we present and evaluate a dissemination system for this particular feeder based on commodity hardware and open-source message-oriented middleware (Apache Qpid). This allows us to assess the feasibility of this approach and to point out the main challenges to be overcome. Copyright 2013 ACM.

Abstract
The complexity of modern software systems entails the need for reconfiguration mechanisms governing 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 endowed 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.

Abstract
Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. Alloy is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to other tools in order to meet such challenges. This paper's proposal, however, is not establishing a link from Alloy to another single tool, but rather to 'plunge' it into the Hets network of logics, logic translators and provers. This makes possible for Alloy specifications to 'borrow' the power of several, non dedicated proof systems. Semantical foundations for this integration are discussed in detail. © 2013 IEEE.

Abstract
This paper presents the encoding of the hybridisation method proposed in [MMDB11, DM13] into the Hets platform. © 2013 Springer-Verlag Berlin Heidelberg.

Abstract
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 formore 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.