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.

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.

 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.

Graph transformation techniques, and the Double-Pushout approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we show how graph transformation can cope with advanced features of service-oriented process calculi, such as several logical notions of scoping (like sessions and pipelines) together with the interplay between linking and containment. This is illustrated by encoding CaSPiS, a recently proposed process calculus with such sophisticated features. We show how to represent the congruence and reduction relations between CaSPiS processes by exploiting concurrent graph transformations over hierarchical graphs.

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.

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 onymous and anonymous nodes to represent respectively types that are identified as names and structures, and defines graph-based relations and operations on types including subtyping, equivalence, 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 graph-based logical foundation of a formal method for verification of and reasoning about oo programs.

Consider an object-oriented model with a class diagram, and a set of object sequence diagrams, each representing the design of object interactions for a use case. This article discusses how such an OO design model can be automatically transformed into a component-based model for the purpose of reusability, maintenance, and more importantly, distributed and independent deployment. We present the design and implementation of a tool that transforms an object-oriented model to a component-based model, which are both formally defined in the rCOS method of model driven design of component-based software, in an interactive, stepwise manner. The transformation is designed using QVT Relations and implemented as part of the rCOS CASE tool.

Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Integration aims at supporting collaborative healthcare workflows (CHWF) for improvement in sharing healthcare information and resources, efficiency of services and patients safety. CHWF are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modelling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We also follow the idea of UML of some visualized models, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work.

Compensating CSP (cCSP) extends CSP for specification and verification of long running transactions (LRTs). The original cCSP is a modest extension to a subset of CSP that does not consider non-deterministic choice, synchronized composition, and recursion. There are a few further extensions, including one by ourselves that includes non-deterministic choice and hiding. However, recursion in cCSP is still not defined, and it remains a challenge to develop a fixed-point theory of process refinement in cCSP. Solving these two problems is important for the development and use of tools in the correct design of programs with LRTs. In this paper, we define the full extension of CSP for modeling LRTs with a failure-divergence semantics and develop a complete partial order of cCSP refinement. This forms a theory of LRTs, corresponding to CSP theory of communicating processes, so that the verification techniques and their tools, such as FDR, can be extended for compensating processes.

In component-based design, a component interface specification describes the guaranteed order in which the provided methods of the component are called and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing reactive interface automata for modeling the interface behavior of reactive components, and active interface automata for active components. The contribution is a composable model of component interfaces that allows static compatibility checking for different kinds of composition of components through their interface models. Algorithms are given for compatibility checking and generating the interface model of a composite component from its execution model.

In component-based design, a component interface specification describes the guaranteed order in which the provided methods of the component are called and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing reactive interface automata for modeling the interface behavior of reactive components, and active interface automata for active components. The contribution is a composable model of component interfaces that allows static compatibility checking for different kinds of composition of components through their interface models. Algorithms are given for compatibility checking and generating the interface model of a composite component from its execution model.

Graph transformation techniques, and the Double-Pushout (DPO) approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this report, we provide a theory of graph transformations for service programming with sessions and pipelines. The theory shows how graph transformation can cope with advanced features of service-oriented computing, such as several logical notions of scoping (like sessions and pipelines) together with the interplay between linking and containment. This is illustrated by encoding CaSPiS, a recently proposed process calculus with such sophisticated features. We first exploit a graph algebra and set up a graph model that supports DPO graph transformations. Then, we show how to represent CaSPiS processes as hierarchical graphs in the graph model and their behaviors as transformation rules over these graphs. Finally, we provide the soundness and completeness results of these rules with respect to the reduction semantics of CaSPiS.

Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches.

In a component-based design, a component interface specification describes the guaranteed ordering in which the component accepts calls to its provided methods and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing the concepts of reactive interface automata (RIA) for reactive components and active interface automata (AIA) for active components. We present a component-based architecture description language for object-oriented and service-based design in which a composite reactive component is built from a number of reactive components and active components through different operators. For the architectural operators, we provide the algorithms for constructing RIA of composite components.