Publications

We present a graph-based model of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Java. In the classical graph theory, we define type graphs, instantiation graphs and conjunction graphs that naturally illustrate the relations among types, generics and interfaces within complex OO programs. The model employs a combination of nominal and anonymous nodes to represent respectively types that are identified by names and structures, and defines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algorithms based on the graph structures are designed for the implementation of the type system. We believe that this type system is important for the development of a graphbased logical foundation of a formal method for verification of and reasoning about OO programs.

Integrating formal methods into UML opens up a way to complement UML-based software development with precise semantics, development methodologies, as well as rigorous verification and refinement techniques. In this paper, we present an approach to integrate a formal method to practical component-based model driven development through defining a UML profile that maps the concepts of the formal method as UML stereotypes, and implementing the profile into a CASE tool. Unlike most of the previous works in this vein, which concentrate on verifying the correctness of the models built in the development process, we focus on how the full development process can be driven by applying the refinement rules of the formal method in an incremental and interactive manner. The formal method we adopt in this work is the refinement for Component and Object Systems (rCOS). We demonstrate the development activities in the CASE tool using an example.

Recently, software verification is being used to prove the presence of contradictions in source code and thus reveal potential weaknesses in the code or provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source code to logic can be very simple and thus easy to solve by automated theorem provers. In this paper, we present a translation of Java into logic that is suitable for proving the presence of contradictions in code. We show that the translation, which is based on the Jimple language, can be used to analyze real-world programs, and discuss some issues that arise from differences between Java code and its bytecode

Recent developments in data de-identification technologies offer sophisticated solutions to protect medical data when, especially the data is to be provided for secondary purposes such as clinical or biomedical research. So as to determine to what degree an approach-- along with its tool-- is usable and effective, this paper takes into consideration a number of de-identification tools that aim at reducing the re-identification risk for the published medical data, yet preserving its statistical meanings. We therefore evaluate the residual risk of re-identification by conducting an experimental evaluation of most stable research-based tools, as applied to our Electronic Health Records (EHRs) database, to assess which tool exhibits better performance with different quasi-identifiers. Our evaluation criteria are quantitative as opposed to other descriptive and qualitative assessments. We notice that on comparing individual disclosure risk and information loss of each published data, mu-Argus performs better. Also, the generalization method is considerably better than the suppression method in terms of reducing risk and avoiding information loss.

We introduce a new quantitative measure of international scholarly impact of countries by using bibliometric techniques based on publication and citation data. We present a case study to illustrate the use of our proposed measure in the subject area Energy during 1996 to 2009. We also present geographical maps to visualize knowledge flows among countries. Finally, using correlation analysis between publication output and international scholarly impact, we study the explanatory power of the applied measure.

consuming part in program debugging. Fault localization techniques can help to automate this task. Particularly promising are static proof-based techniques that rely on an encoding of error traces into trace formulas. By identifying irrelevant portions of the trace formula, the possible causes of the error can be isolated. One limitation of these approaches is that they do not take into account the control flow of the program and therefore miss common causes of errors, such as faulty branching conditions. This limitation is inherent to the way the error traces are encoded. In this paper, we present a new flow-sensitive encoding of error traces into trace formulas. The new encoding enables proof-based techniques to identify irrelevant conditional choices in an error trace and to include a justification for the truth value of branching conditions that are relevant for the localized cause of an error. We apply our new encoding to the fault localization technique based on error invariants and show that it produces more meaningful error explanations than previous approaches.

Free and open source software projects are often perceived to be of high quality. To a great extent the success of open source software seems to be due to an implicit but effective connection between communication and contribution in its development process. In this paper, we present a snapshot of the state the art on quality and success of Open Source Software (OSS) based on a review of the literature. For each of these concepts, we describe various measures considered in the literature and a number of methods by which they are obtained. Contributions to an Open Source Software (OSS) project are made through communication among developers and users. We elaborate on the concrete notions of communication and contribution in Open Source Software (OSS) and their links.

Model-Driven Software Development is nowadays taken as a mainstream methodology. In the software engineering community, it is a synonym of the OMG Model-Driven Architecture (MDA). However, in the formal method community, model-driven development is broadly seen as model-based techniques for software design and verification. Because of the difference between the nature of research and practical model-driven software engineering, there is a gap between formal techniques, together with their tools, and their potential support to practical software development. In order to bridge this gap, we define the meanings of component-based software architectures in this chapter, and show how software architectures are formally modeled in the formal model-driven engineering method rCOS. With the semantics of software architecture components, their compositions and refinements, we demonstrate how appropriate formal techniques and their tools can be applied in an MDA development process.

Nowadays, acquisition of trustable information is increasingly important in both professional and private contexts. However, establishing what information is trustable and what is not, is a very challenging task. For example, how can information quality be reliably assessed? How can sources’ credibility be fairly assessed? How can gatekeeping processes be found trustworthy when filtering out news and deciding ranking and priorities of traditional media? An Internet-based solution to a human-based ancient issue is being studied, and it is called Polidoxa, from Greek “poly” (πολύ), meaning “many” or “several” and “doxa” (δόξα), meaning “common belief” or “popular opinion.” This old problem will be solved by means of ancient philosophies and processes with truly modern tools and technologies. This is why this work required a collaborative and interdisciplinary joint effort from researchers with very different backgrounds and institutes with significantly different agendas. Polidoxa aims at offering: 1) a trust-based search engine algorithm, which exploits stigmergic behaviours of users’ network, 2) a trust-based social network, where the notion of trust derives from network activity and 3) a holonic system for bottom-up self-protection and social privacy. By presenting the Polidoxa solution, this work also describes the current state of traditional media as well as newer ones, providing an accurate analysis of major search engines such as Google and social network (e.g., Facebook). The advantages that Polidoxa offers, compared to these, are also clearly detailed and motivated. Finally, a Twitter application (Polidoxa@twitter) which enables experimentation of basic Polidoxa principles is presented. 

 We present a new automata-based interface model describing the
  interaction behavior of software components. Contrary to earlier
  component- or in\-terface-based approaches, the interface model we
  propose specifies all the non-blockable interaction  behaviors of a
  component with any environment. To this end, we develop an algorithm
  to compute the unblockable interaction behavior, called the
  \emph{interface model of a component}, from its execution
  model. Based on this model, we introduce composition
  operators for the components and prove important
  compositionality results, showing the conditions under which
  composition of interface models preserves unblockable sequences of
  provided services.

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.

We present a new formal validation method for healthcare security policies in the form of feedback-based queries to ensure an answer to the question of Who is accessing What in Electronic Health Records. To this end, we consider Role Based Access Control (RBAC) that offers the flexibility to specify users, roles, permissions, actions, and the objects to secure. We use the Z Notation for formal specification of RBAC security policies and for queries to review these security policies. To ease the effort in creating the correct specification of the security policies, RBAC-based graphical models (such as SecureUML) are used and automatically translated into the corresponding Z specification. Both the specification of the queries and the specification of the policies are then animated using the Jaza tool to execute queries against the specification. By this it is automatically shown who will access the medical record of a patient and what information will be exposed to a system user.