Abstract
This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper's main contribution is to provide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them.

Abstract
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of p -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 f-institutions. © C.J. Rodrigues, M.A. Martins, A. Madeira & L.S. Barbosa This work is licensed under the Creative Commons Attribution License.

Abstract
The complexity of interactions governing the coordination of loosely-coupled services, which forms the core of current software, brought behavioural issues up to the front of architectural concerns. This paper takes such a challenge seriously by lifting typical behaviour modelling techniques to the specification of both types and instances of architectural patterns in which the later ones are connected by ports that behave according to a water flow metaphor. A specific language is introduced for this purpose as well as a translator to mCRL2 so that the simulation and analysis techniques available in the corresponding toolset can be used to reason about (the behavioural layer of) software architectures. The approach is illustrated in a few examples. Copyright 2011 ACM.

Abstract
What sort of component coordination strategies emerge in a software integration process? How can such strategies be discovered and further analysed? How close are they to the coordination component of the envisaged architectural model which was supposed to guide the integration process? This paper introduces a framework in which such questions can be discussed and illustrates its use by describing part of a real case-study. The approach is based on a methodology which enables semi-automatic discovery of coordination patterns from source code, combining generalized slicing techniques and graph manipulation.

Abstract
Over the last decade component-based software development arose as a promising paradigm to deal with the ever increasing complexity in software design, evolution and reuse. Shacc is a prototyping tool for component-based systems in which components are modelled coinductively as generalized Mealy machines. The prototype is built as a Haskell library endowed with a graphical user interface developed in Swing. © 2011 Springer-Verlag.

Abstract
Time series motif discovery is the task of extracting previously unknown recurrent patterns from time series data. It is an important problem within applications that range from finance to health. Many algorithms have been proposed for the task of efficiently finding motifs. Surprisingly, most of these proposals do not focus on how to evaluate the discovered motifs. They are typically evaluated by human experts. This is unfeasible even for moderately sized datasets, since the number of discovered motifs tends to be prohibitively large. Statistical significance tests are widely used in bioinformatics and association rules mining communities to evaluate the extracted patterns. In this work we present an approach to calculate time series motifs statistical significance. Our proposal leverages work from the bioin-formatics community by using a symbolic definition of time series motifs to derive each motif's p-value. We estimate the expected frequency of a motif by using Markov Chain models. The p-value is then assessed by comparing the actual frequency to the estimated one using statistical hypothesis tests. Our contribution gives means to the application of a powerful technique - statistical tests - to a time series setting. This provides researchers and practitioners with an important tool to evaluate automatically the degree of relevance of each extracted motif. Copyright © SIAM.