Quantitative analysis of interacting systems: foundations and algorithms

Summary [5000]

In recent years, there has been an increasing interest in studying the behavior of software systems from a quantitative perspective. Such an interest is actually driven by concrete challenges coming from the engineering practice. It is widely recognized that to suitably meet these challenges requires the development of both solid foundations and derived techniques. Such is the starting point of this project.

As an illustration, consider a service-based application running in a call center performing matching between customers and operators. Typical questions about such system include:

(1) How far is the system with "n" operators from an ideal system where the customer never waits (and the number of free operators is not too high)?

(2) For which values of "n", along the course of the day, are the behaviors of the current system and ideal system closer?

(3) How can customer feedback about the match between the requested service and the offered be used to improve following calls?

Their relevance cannot be understated: the resources needed to keep a system running, such as the number of operators or memory available in a computer, are not infinite and it is of the utmost importance to decrease the use of resources and at the same time keep a reasonable performance. To properly answer this sort of questions, however, entails the need for techniques aimed at analyzing systems from a quantitative perspective, as well as for robust algorithms which implement them.

In broad terms, the analysis of the behaviour of computing devices is an evergreen subject of computer science. Defining “what is the behaviour of a system” or “when two systems behave the same” is a fundamental issue from its dawn till nowadays. Many different (behavioural) equivalences have been introduced for different kinds of systems (e.g., functional, non-deterministic and concurrent systems) and a huge “corpus of conceptual and computational tools” consisting of algorithms, proof’s techniques, rules formats and different sorts of languages has been developed to reason about systems and their behavioural equivalences.

What has recently emerged from the software industrial practice (namely in safety-critical domains and hybrid design) is the need to take into account explicitly, when reasoning about systems' behaviour, quantitative properties, for which existing equivalences are somehow inadequate, since they only allow “boolean reasoning”: either two systems are equivalent or they are not.

Motivated by these considerations, several notions of behavioural metrics or closely related approaches have been proposed. Differently from the ordinary equivalences, behavioural metrics express the distance between the behaviours of systems. A major challenge in this context concerns the fact that many of the conceptual and computational tools mentioned above being not yet available for metrics.

This projects adopts a new approach: it proposes to “lift” such tools from equivalences to metrics by employing the theory of coalgebras. Note that many important tools developed for equivalences are concrete instances of abstract coalgebraic results. On the other hand, the genericity of coalgebraic constructions, which are parametric on the model of the underlying behaviour structure, offers a general setting to frame different sorts of behavioural reasoning, including quantitative modelling, analysis and metrics. Applications of coalgebra theory to probabilistic transition systems lead to the design of one of the most efficient, known algorithms for computing metrics (see [vBW]) which is an encouraging result for our own research programme.

The envisaged contributions are placed at three different levels. First, from a foundational perspective, we propose to advance the state of the art in the theory of metric behavioural equivalences. Secondly, we intend to make the theory operational by developing efficient algorithms to compute the distance between two systems. Such algorithms will be rendered as plug-ins to the core of a prototype tool and its effectiveness tested in an exisiting service-oriented software system. As a third contribution, on the applications side, we intend to add the quantitative dimension (theory and techniques) to Reo, a component based specification language, and use such an enriched framework to analyze and transform service-oriented systems.

A main case-study will be supplied by the dutch company Almende: the ASK system, an industrial software system for connecting service providers and consumers (for instance, the call center example above is one of its instantitations). ASK has been modeled in Reo, which will make possible to use and extend its original model in order to obtain a detailed analysis of the quantitative properties of the system. The outcome of such analysis will help both the developers and the installations of the ASK system to tune resource allocation in order to improve the performance of the system.

Sumário [5000]

O interesse pelo estudo rigoroso do comportamento dos sistemas a partir de um ponto de vista quantitativo tem vindo a crescer quer no campo académico quer na indústria. De facto, tal interesse é motivado por desafios complexos na prática da Engenharia dos sistemas informáticos. É hoje consensual que uma resposta adequada a esses desafios requer o desenvolvimento tanto de fundamentos matemáticos sólidos como das técnicas de análise e verificação deles derivadas. Tal é objectivo deste projecto.

Como ilustração, considere-se uma aplicação baseada em serviços instalada num call center para estabelecimento e manutenção de ligações entre clientes e operadores. Típicas questões neste domínio serão

(1) Qual a distância entre o sistema típico com n utilizadores e um sistema ideal em que o cliente nunca espera (e o número de operadores é livre, embora não excessivo)?

(2) Para que valores de n, ao longo do dia, é que os comportamentos do sistema real e do ideal se aproximam?

(3) De que modo o feedback manifestado por cliente sobre o serviço requerido e o oferecido, é usado para melhoria do nível do serviço?

A relevância destas questões não pode ser iludida: os recursos necessários para manter um sistema activo, tais como o número de operadores e a memória disponível, não são infinitos. É, neste contexto, da maior importância decrementar o uso de recursos e, ao mesmo tempo, manter um nível de desempenho adequado. Para responder as estas questões, contudo, torna-se necessário desenvolver técnicas para análise quantitativa dos sistemas e algoritmos robustos que as implementem.

Em termos gerias, a análise do comportamento dos sistemas computacionais constitui um tópico quente e recorrente de investigação. A definição daquilo que é o comportamento de um sistema ou a indagação sobre se dois sistemas se comportam de forma análoga, é já uma preocupação antiga. Muitas equivalência (comportamentais) foram introduzidas para diferentes tipos de sistemas (e.g., funcionais, não determinísticos ou concorrentes) e um enorme corpus conceptual e de ferramentas, incluindo algoritmos, técnicas de prova, formatos de regras e linguagens, desenvolvido para raciocinar sobre sistemas complexos e suas equivalências comportamentais.

O que emergiu mais recentemente da pratica industrial (nomeadamente em software critico e em sistemas hídricos) foi a necessidade de tomar em consideração de forma explícita, ao raciocinar sobre comportamento, propriedades de natureza quantitativa para as quais as equivalência estudadas na literatura são insuficientes. Estas limitam-se, regra geral, a conclusões booleanas: ou os sistemas são ou não são equivalentes.

Motivadas por este tipo de considerações, diferentes noções de métricas comportamentais, e outras aproximações similares, têm sido propostas. Ao contrário das equivalências comportamentais clássicas, estas métricas quantificam a distância entre comportamentos. No entanto, a maioria das ferramentas computacionais e conceptuais disponíveis não estão equipadas com suporte adequado para este tipo de métricas.

Este projecto adopta uma nova aproximação: propõem-se estender tais ferramentas a métricas, recorrendo à teoria das coalgebras. Note-se que a maior parte das ferramentas orientadas às equivalências clássicas são, de facto, concretizações de resultados abstractos em coalgebras. Por outro lado, a generalidade das construções coalgébrias, paramétrica no modelo escolhido para captar o comportamento subjacente, oferece um contexto formal para enquadrar diferentes tipos de raciocínio comportamental, incluindo modelação quantitativa, análise e métricas. Aplicações da teoria das coalgebras a sistemas de transição probabilísticos levou à concepção de um dos algoritmos mais eficientes para cálculos de métricas (ver [vBW]), o que é um resultado encorajador para o nosso próprio programa de investigação.

O projecto visa contribuir a três níveis distintos. Primeiro, numa perspectiva fundamental, propõe-se fazer avançar o estado da arte na teoria das equivalência com base em métricas comportamentais. Em segundo lugar pretende-se operacionalizar essa teoria através do desenvolvimento de algoritmos eficientes para calcular a distância comportamental entre dois sistemas. Tais algoritmos serão disponibilizados como plug-ins de uma ferramenta de prototipagem e a sua adequação técnica testada com dados (sistemas) reais.

Finalmente, ao nível das aplicações, o projecto propõe-se incorporar a dimensão quantitativa (teorias e técnicas) em Reo e utilizar esta plataforma para analisar e transformar sistemas baseados em serviços.

Uma estudo de caso de dimensão não trivial será fornecido pela empresa holandesa Almende: o sistema ASK. Trata-se de um pacote comercial para interligar fornecedores e clientes de serviços. ASK foi já modelado em Reo, o que torna possível usar e estender esse modelo original para obter uma análise detalhada das propriedades de natureza quantitativa do sistema. Os resultados dessa análise apoiarão quer os que desenvolvem este sistema quer os que o instalam e mantém, no apuramento e controlo da alocação de recursos de forma a melhorar o seu desempenho.

Literature Review [6000]

* Coalgebraic metric bisimulations (relevant for tasks T1, T2 and T3)

Desharnais, Gupta, Jagadeesan and Panangaden [DGJP] proposed a notion of behavioural (pseudo)metric for probabilistic transition systems. Later, van Breugel and Worrel took a more coalgebraic view on the work of [DGJP], providing the connection with linear programming and constructing the final coalgebra in the category of metric spaces and contractive maps. The metric in both papers is defined in the style of Milner-Park’s bisimilarity: it is the greatest fixpoint of a monotone function over the (partially ordered) set of metrics. The work in [vBW] introduces the most efficient algorithm for computing metrics up to date. It is done for a particular type of quantitative system and the results are based on coalgebras. We see this as a witness that the use of coalgebras to achieve the aims of this project is promising.

* Stochastic Reo (relevant for task T4)

Reo [Arb] is a channel-based coordination model wherein so-called connectors are used to coordinate (i.e., control the communication among) com- ponents or services exogenously (from outside of those components and services). In Reo, complex connectors are compositionally built out of primitive channels. Stochastic Reo [MSKA] is an extension of Reo where channel ends and channels are annotated with stochastic values for data arrival rates at channel ends and processing delay rates on channels. Such rates are, e.g., non-negative real values that describe how the probability that an event occurs varies with time. As a specification language Reo is intuitive and it has been applied to real systems, including the one mentioned in T4. However, the focus on the research on Reo and its variants has been on modelling and expressiveness and no work on equivalence reasoning has been done so far. We believe that the results of this project will add value to the theory and tools available for Reo.

* QoS? of distributed systems(relevant for T4 and T5)

The project identifies a specific application area: the development of a calculus of QoS? -robust composition of software services, resorting to the concepts and techniques delivered by the Tasks T1 to T3. With the growing complexity and size of modern distributed systems, the need for models to support their architectures, design their coordination, and manage their QoS? at run time has become a critical issue. To build large-scale distributed applications, one often needs to select components/services from a set of functionally equivalent candidates, meaning, those that implement the same functionality but differ in their non-functional characteristics, i.e., QoS? properties. Therefore, a important aspect of service composition relates to the management of the QoS? requirements, a topic clearly in the scope of application of the present proposal.

QoS? of distributed systems refers to a wide range of quality metrics, including, for example, availability, reliability, security, flexibility, performance (response time, for instance), and so on (see e.g. [LBNDKC]). Over the past few decades, several quantitative stochastic methods (e.g., stochastic Petri Nets, interactive Markov Chains) have been proposed and used in a variety of application areas to study different QoS? metrics. Different kinds of extensions of process algebras have been developed for performance evaluation, including timed process algebras, probabilistic process algebras, and stochastic process algebras. These process algebra-based approaches are compositional at a fine-grain level, which makes them difficult to use them for composing services in an architecturally meaningful way as black boxes. Coordination based models, such a Reo, in which both application in T5 and case study in T4 will be framed, provides a more structural approach to interaction control. In general, however, and to a large extent, existing formal models for service composition lack sound, pragmatic means for reasoning about QoS? properties.

It is expected this project contributes to further extending current models and techniques to make them suitable for architecture-based assessment and monitoring of the end-to-end QoS? of large-scale service-oriented applications. Specifically, the project aims at defining a QoS? -aware architectural model on top of Reo and a notion of robust service composition. Preliminary results obtained within the project team are reported in [MB]. QoS? -robustness is intended to measure the quality of response to unpredictable change and avoidance of failure. Robustness is studied in several contexts. Relevant to the approach this project aims at exploring is research on game-theoretic semantics. Game-theoretic approaches [Abr] enable a fine-grained understanding of the logical principles underlying interaction based on the system’s structure, which may provide an interesting alternative to model endurance to failure.

* The team's research.

The team has extensive research in coalgebraic methods in computer science [BRS,Mon,Mon98,BM09] and quantitative models, which frames the research proposal in tasks T1, T2 and T3. From the applicational side, with relevance to tasks T4 and T5, the team is also recognized for contributions in models and calculi for component-based and service-oriented software [RB,BB] and QoS analysis [BBRS,MB,MSKA,SBRS].

Plan and Methods [10000]

Reasoning about the behavior of software systems is a topic that has occupied computer scientists since the beggining of the field. For many years, the formal methods community has focussed on critical software systems, such the ones running on an airplane or space shuttle, and techniques such as model-checking are by now well-established and effective in assessing the validity of crutial properties. In the last few years, attempts on tranferring these techniques too mainstream software systems have been made, but they were shown innaproppriate: for most systems, one does not want a property to hold, but instead one wants to assess that a certain property holds in 99% of the cases. Think of the call center example in the summary: the company does not strictly want that clients never wait more than 1 minute, but instead they want to ensure, for instance, that in 90% of the cases this happens.

This type of ``quantitative reasoning'' is now gaining popularity and in the next few years it will be one of the most relevant topics in Computer Science research.

Our proposal fits in this line of research and we are aware that any relevant contribution

• requires solid foundational work
• as well as relevant empirical work, with concrete case studies and tools illustratting the effectiveness of the approach

Therefore, this proposal contains:

(1) Two foundational tasks, contributing to the state of the art in reasoning about the equivalence of quantitative models.

(2) One operational task, in which efficient algorithms to compute the equivalences derived in (1) will be devised.

(3) One case study, where we intend to transfer the techniques developed to a real software system. This empirical work will be developed jointly with the dutch company Almende.

(4) One application-oriented task, in which theoretical results, techniques and tools developed in the project are integrated to address a relevant and difficult problem in service-oriented design: the characterization QoS-robustness for services and an associated calculus of QoS-robust composition.

In the sequel, we explain the essence of our approach and the potential of the research team.

Vision

Both from a theoretical and a technological point of view, global computing raises a number of challenging and difficult research questions whose relevance for the future of Software Engineering cannot be underestimated. On the theory side, examples include the quest for interaction models, coordination calculi, foundations for co-operation and mobility, resource usage and security, semantics and methods for service specification, orchestration and deployment, among many others.

On the other hand, long term research in coalgebra theory and coindution provided an useful set of both conceptual and methodological tools to study the the semantics of reactive, interactive and mutable systems.

The envisaged approach in this project touchs upon several sides of the research spectrum: foundational, applicational and experimental.

At a foundational level, the project will introduce new notions of equivalence, more appropriate to reason about quantitative properties of models of computation. In short, at this level, our approach will be coalgebraic. The strength of the coalgebraic approach lies in the fact that notions are developed uniformly parametrized on the type of the system, which enables the development of notions and tools for a large class of models at the same time.

At the applicational level, we will devise efficient algorithms to compute the equivalences developed in the previous point and develop prototype tools, to be made available publicly.

At the experimental level, the project aims at applying all the techniques developed at the other two levels to a real case study. This will validate the general framework and show its generality does not constrain its application.

In short, this proposal combines foundational research with engineering work, the latter supported by a Dutch software company, Almende. It fosters the cooperation between two national groups at the University of Minho and University of Lisbon, who already share interest in coalgebraic semantics, but have complementary skills. The groups have jointly organized a series of Joint Research Workshops on ``Coinduction, Interaction and Composition'', which brought together research groups on both coalgebraic methods and their application to the development of models and calculi for interaction, composition and coordination of software components and services.

The team

This research program builds upon the team's extensive research on

• coalgebraic methods in computer science [BRS,Mon,Mon98,BM09],
• analysis of quantitative models and QoS? -aware formal methods [BBRS,MB,MSKA,SBRS,MO].

The foundational results and techniques to be developed in Tasks T1, T2 and T3, will be applied to a hot research topic in the semantics of service-orientation (T5) and to a related case study (T4). Again this is rooted on the team's previous work on

• models and calculi for software interconnection and architectures [BB,RB,BCS,BCS11]

Dynamic reconfigurable service architectures is precisely the topic of another FCT-funded project (Mondrian - PTDC/EIA-CCO/108302/2008), coordinated by a member of this team. Actually, one of the motivations for this proposal came from current research in Mondrian: crescent awareness of the role of QoS? measures to drive software reconfiguration and, correspondingly, the need for effective techniques and algorithms for formal quantitative analysis.

The team previous work will be further strengthened by the involvement of Prof.dr. F. Arbab (CWI), the inventor of Reo, and with whom we have on-going collaboration, Prof.dr. P. Panangaden (McGill), an expert on Markov processes, and Prof.dr. C. Baier, an expert on probabilistic model-checking. Previous work, namely in the context of European projects, with the proposed consultants, bears sustainability to the envisaged collaboration.

The elements of the team have supervised a number of PhD? projects in related areas, posses an interesting publication record and maintain close collaborations with leading research international groups (eg the Foundations of Software Engineering cluster at CWI, Amsterdam, the group of Dexter Kozen, at Cornell University and the Comete group, headed by C. Palamidessi, at INRIA).

Two additional aspects should be mentioned about the team. First, by combining synergies of the two portuguese research groups on coalgebra theory and applications (in Minho and Lisbon), the project has the potential to establish of a new, pioneering area of expertise for both groups at University of Minho and New University of Lisbon. It is, thus, a starting point for the near future, but rooted, as mentioned above, in a previous series of joint seminars and workshops organized every year since 2006.

A second aspect concerns the team choice for PI: a recent, post-doc fellow at UM, with a remarkable record of publications in the project's target area, will serve as project coordinator. QUAIS is expected to frame her post-doc training in a broader context and to boost a new, exciting research area (that of coalgebraic foundations and techniques for quantitative analysis of interactive systems) on top of a well-established domain (that of coalgebraic methods) in which both the PI and Minho-Lisbon teams have relevant contributions. This corresponds to our vision of on the role of a post-doc fellow in the national scientific network.

Tasks

• T1 - Uniform metric derivation for models of computation
• T2 - Distances via coalgebraic metric bisimulation
• T3 - Computational layer: algorithms to compute metric bisimulations
• T4 - Case study: the ASK system
• T5 - Application: a QoS-robust composition calculus for services

Timeline and Management

Most management effort will be dedicated to ensure that tasks proceed according to the established plan, and that milestones are delivered on time. Special care will be taken with critical milestones, on which other tasks depend. Such is the case of milestone ...

The following activities are planed in order to ensure coordination between team members:

- A bi-monthly seminar, alternating between UM and UNL, will be held with all members active in the project at the time;

- Each of these meetings will be complemented with a technical presentation by one of the project members; these talks will be open to the research community and each project member is required to give at least one such talk;

-A research workshop will be held every year, in September, to assess the project progress and provide a forum, open to the scientific community to present and validate work-in-progress.

- A collaborative site will be launched at the start of the project; besides serving as the main diffusion point of the project, it will include a private area to share documents and scribble current research ideas.

The team considers extremely relevant to the success of this project and to the international dissemination of its results, the role of consultants (see below justifications and tasks assigned).

To maximize the revenue from the project budget, the following measures will be taken:

- Submissions to conferences will follow according to a plan defined by the PI, in order to avoid spending the mission budget in events which are not relevant to the project; this plan will mainly include first tier international conferences mentioned in the individual task descriptions.

- To fully benefit from consultants expertise, each visit will start with a one-day informal workshop where all active team members are expected to give a short talk; by these we expect the consultant to get acquainted with the overall project status, thus increasing the potential for effective and relevant scientific discussions;

- Apart from the usual meetings with their designated supervisors, all BI grant holders will be requested to submit every 3 months a progress report to ensure that the research plan is progressing as expected.

One senior management official will be designated by each partner (UM and UNL) to help with financial planning, and progress/final reports to FCT.

Some ideas for milestones:

1. M1: Coalgebraic metrics (preliminary results on tasks T1 and T2; workshop with consultants C. Baier and P. Panangaden)

1. M2: Prototype tool (Prototype tool (T3))

1. M3: Calculus of QoS? -robust service composition (Modelling language plus simulator (T5))

1. M4: Case study (Experimental report on the analysis of the ASK system (T4); workshop with consultants F. Arbab and C.Baier)

Past Publications [5]

[BBRS] Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, Alexandra Silva: Deriving Syntax and Axioms for Quantitative Regular Behaviours. CONCUR 2009: 146-162, Springer

[Mon] Luís Monteiro: A Coalgebraic Characterization of Behaviours in the Linear Time - Branching Time Spectrum. WADT 2008: 251-265

[MSKA] Young-Joo Moon, Alexandra Silva, Christian Krause, Farhad Arbab: A Compositional Model to Reason about end-to-end QoS in Stochastic Reo Connectors. Science of Computer Programming. 2011. Accepted for publication.

[RB] Nuno F. Rodrigues, Luís Soares Barbosa: Slicing for architectural analysis. Science of Computer Programming 75(10): 828-847 (2010)

[SBBR] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten: Quantitative Kleene Coalgebras. Information and Computation. 2011. In Press.

Bibliographic References [30]

[Abr] S. Abramsky. Algorithmic game semantics: A tutorial introduction. In H. Schichtenberg and R. Steinbruggen, editors, Proceedings of the NATO Advanced Study Institute, Marktoberdorf, pages 21–47. Kluwer Academic Publishers, 2001

[Arb] F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science (MSCS) 14(3):329-366 (2004)

[ABBR] F. Alessi, P. Baldan, G. Bellè, and J. J. M. M. Rutten. Solutions of functorial and nonfunctorial metric domain equations. Electr. Notes Theor. Comput. Sci., 1, 1995

[BB] Marco Barbosa, Luís Soares Barbosa: A perspective on service orchestration. Science of Computer Programming 74(9): 671-687 (2009)

[BM09] Luís Soares Barbosa and Sun Meng: A coalgebraic semantic framework for reasoning about interaction designs in UML2 Semantics and Applications, Kevin Lano (ed), John Wiley and Sons, Inc., pp 249-279 (2009)

[BSdV] Falk Bartels, Ana Sokolova, Erik P. de Vink: A hierarchy of probabilistic system types. Theor. Comput. Sci. 327(1-2): 3-22 (2004)

[BM] F. Bonchi and U. Montanari. Minimization algorithm for symbolic bisimilarity. In ESOP, volume 5502 of LNCS, pages 267–284. Springer, 2009.

[BvBR] M. M. Bonsangue, F. van Breugel, and J. J. M. M. Rutten. Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding. Theoretical Computer Science, 193(1-2):1–51, 1998.

[BCS] M. M. Bonsangue, D. Clarke and A. Silva. Automata for Context-dependent Connectors.Accepted for Coordination 2009. In J. Field and V. Vasconcelos, editors, proceedings COORDINATION 2009, LNCS 5521, Springer, 2009, pp. 184--203.

[BCS11] M. M. Bonsangue, D. Clarke and A. Silva. A model of context-dependent component connectors. Science of Computer Programming. In press.

[BRS] M. M. Bonsangue, Jan J. M. M. Rutten, Alexandra Silva: An Algebra for Kripke Polynomial Coalgebras. LICS 2009: 49-58

[vBW] F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115–142, 2005

[DGJP] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled markov processes. Theoretical Computer Science, 318a(3):323–354, 2004.

[DJGP] J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Logic in Computer Science, pages 413–422. IEEE, 2002.

[FM] J.-C. Fernandez and L. Mounier. “on the fly“ verification of behavioural equivalences and preorders. In CAV, volume 575 of LNCS, pages 18a1–191. Springer, 1992.

[Her] U. Herzog: Formal Description, Time and Performance Analysis. A Framework. Entwurf und Betrieb verteilter Systeme 1990: 172-190

[Hir] D. Hirschkoff. On the benefits of using the up-to techniques for bisimulation verification. In TACAS, volume 1579 of LNCS, pages 285–299. Springer, 1999.

[LBNDKC] Liangzhao Zeng, Boualem Benatallah, Anne H.H. Ngu, Marlon Dumas, Jayant Kalagnanam, and Henry Chang. QoS? -Aware Middleware for Web Services Composition. IEEE Transactions on Software Engineering, 30(5):311–327, 2004

[LS] K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991.

[JY] B. Jonsson and W. Yi. Compositional testing preorders for probabilistic processes. In LICS, pages 431–441. IEEE, 1995.

[MO] H. Macedo, José Nuno Oliveira. Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra. In MPC, volume 6120 of LNCS, pages 271–287. Springer, 2010.

[Mon98] Luís Monteiro: Semantic domains based on sets with families of equivalences. Electr. Notes Theor. Comput. Sci. 11: (1998)

[MB] Sun Meng, Luís Soares Barbosa: Towards the introduction of QoS information in a component model. In 2010 ACM SAC, pages 2045–2046. ACM, 2010.

[PHW] A. D. Pierro, C. Hankin, and H. Wiklicky. Quantitative relations and approximate process equivalences. In CONCUR, volume 2761 of LNCS, pages 271–287. Springer, 2003.

[Rut98] J. J. M. M. Rutten. Relators and metric bisimulations. Electr. Notes Theor. Comput. Sci., 11, 1998.

[Rut00] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000.

[Rut07] J. J. M. M. Rutten. Coalgebraic foundations of linear systems. In CALCO, volume 4624 of LNCS, pages 425–446. Springer, 2007.

[SL] R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. In CONCUR, volume 836 of LNCS, pages 481–496. Springer, 1994.

[TR] D. Turi and J. J. M. M. Rutten. On the foundations of final coalgebra semantics. Mathematical Structures in Computer Science, 8(5):481–540, 1998.

[Wor] J. Worrell. Coinduction for recursive data types: partial orders, metric spaces and omega-categories. Electr. Notes Theor. Comput. Sci., 33, 2000.

Publications

2014-2015

Nuno Oliveira, Luís Soares Barbosa: Reasoning about software reconfigurations: The behavioural and structural perspectives. Science of Computer Programming, 110, pp 78–103, 2015.

Renato Neves, Alexandre Madeira, Manuel A. Martins, Luís Soares Barbosa: Proof theory for hybrid(ised) logics. Revised selected papers form SBMF'14. Science of Computer Programming (in print), 2015.

Daniel Murta, JN Oliveira. A study of risk-aware program transformation. Science of Computer Programming. 110:51-77, 2015.

JN Oliveira, V.C. Miraldo. ``Keep definition, change category'' - a practical approach to state-based system calculi. JLAMP, submitted (state=minor revision)

L. Monteiro, Determinization and Bialgebraic Semantics. Technical Report UNL, 2015.

Nuno Oliveira, Alexandra Silva, Luís Soares Barbosa: Quantitative analysis of Reo-based service coordination. ACM, SAC 2014: 1247-1254

JN Oliveira, Metaphorisms in Programming. In RAMICS 2015, volume 9348 of LNCS, pages 171-190. Springer, 2015. DOI: 10.1007/978-3-319-24704-5_11

Alexandre Madeira, Manuel A. Martins, Luís Soares Barbosa: A logic for n-dimensional hierarchical refinement. Refine 2015 (18th International Refinement Workshop, FM'15, Olso, in EPTCS (in print), 2015.

Renato Neves: Logics and Calculi for Cyber–Physical Components. Proc CALCO Early Ideas, LIPICS, Dagstuhl Publishing, 2015.

Renato Neves: On a Monadic Encoding of Continuous Behaviour. Proc. 15th International Conference on Relational and Algebraic Methods in Computer Science - RAMiCS? (ST). CEUR-WS, vol 1454, pp 43-52, 2015.

Victor Miraldo, Object Oriented Programming with Monadic Mealy Machines. QAIS Project, TR-HASLab:03:2014. October 2014.

L. Monteiro, Determinization and Bialgebraic Semantics. CALCO EI 2015.

Thesis

Nuno Oliveira: Architectural reconfiguration of interacting services. PhD? Thesis, MAP-i, Universidade do Minho, Mar 2015.

Ricardo Guilherme Pratas: A Coalgebraic Approach to Fuzzy Automata Theory, Tese de mestrado, 2015.

Vitor Miraldo: Proof by Rewriting in Agda, Tese de mestrado, 2015.

Invited Talks (2015):

Luis Soares Barbosa: Formal methods for thrustworthy eGov infrastructures. Workshop on Innovation and Smart Cities, Universidad Externado de Colômbia, Bogotá, Colombia, July 2015.

Luis Soares Barbosa: Formal models in software design. UYMS 2015, Izmir, Turkey, Sep 2015.

2013-2014

J.N. Oliveira. A relation-algebraic approach to the "Hoare logic" of functional dependencies. Journal of Log. Algebraic Programming, 2014 DOI:10.1016/j.jlap.2014.02.013.

J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. Journal paper. IJFSC Vol. 24, No. 6 (2013), 709-728, World Scientific Pub. Comp. http://dx.doi.org/10.1142/S0129054113400145.

M Bonsangue, G Caltais, EI Goriac, D Lucanu, J Rutten, A Silva. Automatic equivalence proofs for non-deterministic coalgebras. Science of Computer Programming 78 (9), 1324-1345

J.N. Oliveira. Relational algebra for ``just good enough" hardware. In RAMiCS? , volume 8428 of LNCS, pages 119-138. Springer Berlin / Heidelberg, 2014.

Daniel Murta, José Nuno Oliveira: Calculating risk in functional programming. CoRR? abs/1311.3687 (2013)

A. Sanchez, L. S. Barbosa and D. Riesco. Verifying bigraphical models of architectural reconfigurations. In Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE'13, IEEE Press, pp 135-138. 2013.

JB Jeannin, D Kozen, A Silva. Language constructs for non-well-founded computation. In Proceedings of Programming Languages and Systems (ESOP 2013), 61-80, LNCS, Springer, 2013.

A Silva, B Westerbaan. A coalgebraic view of epsilon-transitions In Proceedings of Algebra and Coalgebra in Computer Science (Calco 2013), 267-281, LNCS, Springer, 2013.

F Bonchi, G Caltais, D Pous, A Silva. Brzozowski’s and Up-To Algorithms for Must Testing. In Proceedings of Programming Languages and Systems (APLAS 2013), 1-16, LNCS, Springer, 2013

B Jacobs, A Silva. Initial Algebras of Terms, with binding and algebraic structure. In Lambek's festschrift, LNCS, Springer, 2014.

N. Foster, D. Kozen, M. Milano, A. Silva, L. Thompson. A Coalgebraic Decision Procedure for NetKAT? . Technical report. Cornell University.

D. Murta and J.N. Oliveira. Calculating fault propagation in functional programs. Technical Report TR-HASLab:01:2013, May 2013.

2012-2013

Jean-Baptiste Jeannin, Dexter Kozen and Alexandra Silva CoCaml? : Programming with Coinductive Types Technical Report 1813/30798, Cornell University 2012.

Alexandra Silva, Filippo Bonchi, Marcello Bonsangue and Jan Rutten. Generalizing determinization from automata to coalgebras. In Logical Methods in Computer Science, vol. 9(1), 2013. http://arxiv.org/pdf/1302.1046v2.pdf

José N. Oliveira: Typed Linear Algebra for Weigthed (Probabilistic) Automata. In Proceedings of the 17th International Conference on Implementation and Application of Automata, CIAA 2012, Springer, LNCS.

Bart Jacobs, Alexandra Silva and Ana Sokolova. Trace Semantics via Determinization. In Proceedings of the 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2012), Springer, LNCS.

Filippo Bonchi, Marcello M. Bonsangue, Georgiana Caltais, Jan J. M. M. Rutten, Alexandra Silva: Final Semantics for Decorated Traces. Electr. Notes Theor. Comput. Sci. 286: 73-86, Elsevier

Ana Paula Maldonado, Luís Monteiro, Markus Roggenbach: Towards Bialgebraic Semantics for the Linear Time - Branching Time Spectrum. Recent Trends in Algebraic Development Techniques - 20th International Workshop, WADT 2010: 209-225

Dexter Kozen and Alexandra Silva. Practical Coinduction. (Technical Report)

Jean-Baptiste Jeannin, Dexter Kozen and Alexandra Silva. Language constructs for non-well-founded computation. (Technical Report)

Dexter Kozen and Alexandra Silva. Left-handed completeness. In 13th International Conference on Relational and Algebraic Methods in Computer Science , Cambridge, UK, Springer, LNCS.

Filippo Bonchi, Marcello Bonsangue, Jan Rutten and Alexandra Silva. Brzozowski's Algorithm (Co)Algebraically. In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, Springer, LNCS.

L. S. Barbosa, Sun Meng, "A Calculus for Generic, QoS? -Aware Component Composition " in Mathematics in Computer Science, Springer, 2012 (to appear), DOI 10.1007/s11786-012-0137-2

T2 - Coalgebraic Metric Bisimulation

Bisimulations are an extremely useful tool for reasoning about the equivalence of systems: in order to prove that two systems are behaviourally equivalent, it is enough to provide a bisimulation relating them. The theory of coalgebras provides a general definition of bisimulation [Rut00].

The growing interest in quantitative properties has motivated the definition of quantitative models and related notions of behavioural equivalences (e.g., [LS,JY,SL]). For many quantitative properties, equivalences are somehow inadequate since they only allow ``boolean reasoning'': either two systems are equivalent or they are not. As an example, consider the systems S and Sε, where the latter is like S but with ε-perturbations on quantities. These systems do not behave exactly the same but, for small ε, they behave almost the same, meaning that the behavior of Sε converges to the behaviour of S when ε tends to 0.

Motivated by these considerations, many authors have recently proposed several behavioural metrics or closely related notions (e.g. [DGJP,vBW,PHW]). Differently from the ordinary equivalences, behavioural metrics express the distance between the behaviours of systems: if the distance is 0, then the systems are behaviourally equivalent. Amongst the several proposals, the approach of [DJGP,PHW] is relevant for our proposal. In these papers, they define a pseudometric like Milner-Park's bisimilarity: it is the greatest fixpoint of a monotone function Phi over the (partially ordered) set of metrics. The function Phi relies on the so called Kantorovich metric (also known as Hutchinson, Varstein, transport and earthmover's metric).

Following [Rut98,Wor], we hope to get an abstract notion of metric bisimulation that corresponds to the post-fixed point of the function Phi (described above). These are, in our opinion, extremely innovative and powerful tools for over-approximating the distance of two systems. More formally, if R is a metric bisimulation and dF is the behavioural metric, then R(S1,S2)=ε implies that dF(S1,S2)<=ε.

Recently, in [Mon] the linear spectrum of equivalences was characterized by relaxing the notion of finality to a weaker notion of quasi-finality. This notion, when extended to the metric setting, will provide coarser equivalences than that of bisimilarity.

Main contributions:

• a notion of coalgebraic metric bisimulation for a large class of systems (in particular, for the ones considered in T1)
• a linear spectrum for metric equivalences

Deliverables: Similarly to T1, this task is of foundational character, and, therefore, the main deliverable will be 3 research papers, two of which in a mainstream TCS conference (such as CONCUR, STACS or CALCO) and the other in a journal (such as TCS, MSCS, Information & Computation) plus a PhD and a master thesis.

Research team: LM,AMS,LSB,JNO,EF,APM,NO,BI2

T4 - Case study: the ASK system

The main goal of the ASK system is to do the matching in an efficient way. To achieve that, the system collects feedback on the quality of services after the connection. Such feedback is used to decide better connections for the subsequent requests of the same type. In addition, the system uses self-learning and self-organizing mechanisms by continuously adapting to users' preferences and available resources.

When people request a certain service from specialists or service providers, the ASK system attempts to select the best service provider. This selection is based on the rating of the knowledge and the skills of service providers who are available at that moment. This rating, in turn, is based on the feedback on the quality of services offered by the service providers.

Moreover, the occurrence of events can follow either regular schedules or ad-hoc schedules. The ASK system deals with both of the situations while satisfying the constraints and the purposes of users' requests.

So far, we have abstractly described the ASK system as an agent to provide the connection between service providers and service consumers in an ``efficient'' way. It should be noted that at each time not only one connection is handled. From the architecture perspective, the ASK system is designed as a hierarchical modular system, i.e., it is divided into a number of components taking account into higher level functionalities, and each component is also divided into a number of threads taking into account lower level functionalities. In order to handle massive connections, the components need to have multiple threads that have the same functionalities so that the connections are handled concurrently. In such cases, to provide efficient connections for all users is not trivial.

What is meant by efficiency can be defined and calculated in various ways, i.e., according to the various constraints of quality of services. The result of this calculation, so-called performance evaluation, is better and better when a system has more and more resources. However, in reality, resources are limited. Thus, it is important to show how to obtain the best performance, or more practically a reasonable performance, using limited resources. For instance, consider the call center example from the summary. It is important to keep the waiting time of customers under a reasonable amount of time. Since the number of operators that the call center can employ is limited, they need to be allocated according to the rate of calls during the day. In order to do this, a quantitative evaluation of the number of calls and waiting time can help.

The ASK system has been modeled in Reo. Using that model, extended with rates extracted from the logs of the system, we intend to instantiate the notions defined in T1 and T2 in order to answer questions about resource allocation (such as the questions in the summary). In order to do that we will also extend the Reo model with ``ideal'' rates, i.e. we will create a reference model which we will compare with the actual running model. Furthermore, the notion of distance, from T2, can be used to help improving the ASK system service matching functionality. We will implement this together with Almende.

Main contributions:

• An ``ideal'' Reo model of the ASK system, built in collaboration with the engineers at Almende.
• A Reo model of several running instances of the ASK system. This will imply statistical analysis of the logs of the system in order to extract the rates.
• Analysis of several desirable properties of the system, from which several guidelines to optimize resource allocation should come out.

Research team: BI 6M

Deliverables: case study paper in a mainstream conference (such as WS-FM or FMOODS); a workshop paper; integration of the tool developed in T3 and the ECT tools (this is the toolset wherein Reo models can be defined) and one PhD? thesis (Alejandro Sanchez).

Research Team

• Alexandra Silva
• Alejandro Sanchez
• Ana Maldonado
• Elisabete Freire
• José Nuno Oliveira
• Luís Monteiro
• Luís Barbosa
• Nuno Oliveira
• Daniel Murta (grant holder)

Collaborators

• Ana Sokolova (USalzburg, AU)
• Filippo Bonchi (ENS Lyon, FR)

Consultants

• Christel Baier (Dresden, DE)
• Farhad Arbab (CWI, NL)
• Prakash Panangaden (McGill, CA)

50 Recent Changes in TWiki Web retrieved at 18:33 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Quantitative analysis of interacting systems: foundations and algorithms

Project Summary

In recent years, there has been an increasing interest in studying the behavior of software systems from a quantitative perspective. Such an interest is actually driven by concrete challenges coming from the engineering practice. It is widely recognized that to suitably meet these challenges requires the development of both solid foundations and derived techniques. Such is the starting point of this project.

(read more)

Project Info

• Research/QAIS Web
• Create New Topic
• Index
• Search
• Changes
• Notifications
• Statistics
• Preferences

• Main Webs

•  DI
•  EL
•  Education
•  Events
•  JoseLuisSilva
•  Personal
•  Research

Research/QAIS Web Preferences

The following settings are web preferences of the Research.QAIS web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

• Set WEBTOPICLIST = Home

• Set WEBTITLE = QAIS

• Set SKIN=nat

• Set SKINSTYLE = Kubrick
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE = QAIS

• Set NATWEBLOGO = Qais
• Set WEBLOGOALT =
• Set WEBLOGOURL = WebHome

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the TWiki.Research/QAIS web:

• Web specific background color: (Pick a lighter one of the StandardColors)
  • Set WEBBGCOLOR = #D0D0D0

• List this web in the SiteMap:
  • If yes, set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Make sure to list only links that include the name of the web, e.g. Research/QAIS.Topic links.
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = QAIS
  • Set SITEMAPUSETO = Quantitative analysis of interacting systems: foundations and algorithms

• Exclude web from a web="all" search: (Set to on for hidden webs)
  • Set NOSEARCHALL =

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Research/QAIS web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW = LuisSoaresBarbosa, AlexandraSilva, LuisMonteiro, JoseNunoOliveira, RicardoAlmeida
  • #Set DENYWEBCHANGE =
  • Set ALLOWWEBCHANGE = LuisSoaresBarbosa, AlexandraSilva, LuisMonteiro, JoseNunoOliveira, RicardoAlmeida
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = AlexandraSilva

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = AlexandraSilva
  • Set ALLOWTOPICRENAME = AlexandraSilva

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • # Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Overview

• Home
• Project Description

Team

• Research Team
• Job Opportunities

Results

• Publications
• WorkBench
• (Bi)simulations in KAT
• Project Workshops

Create New Topic in Research/QAIS Web

Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.

Grant BI1-2012_PTDC/EIA-CCO/122240/2010_UMINHO

WP1 - Calculating fault propagation in functional programs

This site contains the experimental part of the homonym paper by D.R. Murta, and J.N. Oliveira (submitted).

Please download and unzip file website.zip first and then move to the just created directory website.

For the Haskell part run

ghci -XNPlusKPatterns paper_haskell_matlab

and follow the examples in Part I of paper_haskell_matlab.pdf

For the MATLAB part, open MATLAB in the same directory, where all the executables can be found, and run Part II of paper_haskell_matlab.pdf

Please report comments, bugs etc to Daniel Murta (danielrpmurta@gmail.com) or Jose Oliveira (jno@di.uminho.pt).

WP2 - Faults which interfere with termination

(...dually: programs which shouldn't terminate and sometimes do so...) On-going work, requires sub-distributions.

WP3 - Calculating fault propagation in component-oriented software

Paper: J.N. Oliveira. Preparing Relational Algebra for "Just Good Enough" Hardware. In RAMiCS, volume 8428 of LNCS, pages 119-138 (DOI: 10.1007/978-3-319-06251-8_8) Springer Berlin / Heidelberg, 2014. (Slides of the presentation.)

NB: In the experiments underlying this paper we are using a probabilistic extension of a monadic library written in Haskell for the component coalgebraic combinators of Barbosa's PhD thesis: see the MMM Libray.