Cláudio Belo Lourenço

This paper studies complex coordination mechanisms based on constraint satisfaction. In particular, it focuses on data-sensitive connectors from the Reo coordination language. These connectors restrict how and where data can flow between loosely-coupled components taking into account the data being exchanged. Existing engines for Reo provide a very limited support for data-sensitive connectors, even though data constraints are captured by the original semantic models for Reo. When executing data-sensitive connectors, coordination constraints are not exhaustively solved at compile time but at runtime on a per-need basis, powered by an existing SMT (satisfiability modulo theories) solver.To deal with a wider range of data types and operations, we abstract data and reduce the original constraint satisfaction problem to a SAT problem, based on a variation of predicate abstraction. We show soundness and completeness of the abstraction mechanism for well-defined constraints, and validate our approach by evaluating the performance of a prototype implementation with different test cases, with and without abstraction.

Checking language equivalence (or inclusion) of nite automata is a classical problem in Computer Science, which has recently received a renewed interest and found novel and more eective solutions, such as approaches based on antichains or bisimulations up-to. Several notions of equivalence (or preorder) have been proposed for the analysis of concurrent systems. Usually, the problem of checking these equivalences is reduced to checking bisimilarity. In this paper, we take a diferent approach and propose to adapt algorithms for language equivalence to check one prime equivalence in concurrency theory, must testing semantics. To achieve this transfer of technology from language to must semantics, we take a coalgebraic outlook at the problem.

Open Government is a new trend in public governance, based on the principles of transparency, collaboration and participation, currently being adopted by many countries around the world including 63 members of the Open Government Partnership. Operationalizing such principles requires developing certain capabilities among citizens and relevant government actors. For example, participation requires citizens to be informed and engaged, and achieving this requires government to build capabilities in using appropriate tools for informing and engaging. This poster paper outlines a research work in progress for developing an e-Participation toolkit called WeLEaD - Collaborative Toolkit for Learning, Engaging and Deciding. The toolkit will comprise an integrated set of advanced e-participation tools, based on the peer-production approach to collaborative teaching and learning: 1) to help citizens learn from each other about relevant issues on the public policy agenda; 2) to engage policy-makers, government executives, citizens and other non- state actors in informed discussions on how to advance this agenda; and 3) to reflect the outcomes of such discussions, including citizen views and opinions, in government's policy- making processes. The toolkit will also include technical and organizational guidelines for conducting e-Participation initiatives, including the use of such tools.

Social graphs can be used to express personal relationships between internet users. Query the entire network is a very expensive task and here is no interest to continue a query when a successfully answer is already known. This paper proposes a searching mechanism to query nodes in several social graphs topologies. Active users are continuously expanding the social network, resulting in frequent changes on the social graph topology. The results show that expanded social circles are an efficient query mechanism and resilient to distinct social graph models.

This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.

We present PVSio-web which extends the simulation component of the PVS proof system with functionalities for rapid prototyping device user interfaces. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of the device user interface under development, specify interactive areas over the layout, and link them to a PVS specification. They can then explore the behaviour of the formal user interface specification through point-and-click interactions. The architecture of the tool is general, and can be used as the basis for extending other verification tools. A demonstration of the capabilities of PVSio-web is presented through an example based on a commercial medical device user interface. Our ultimate aim is to promote and facilitate the use of formal verification tools when developing device user interfaces.