Publications

We present a model for component software. We describe how components are specified at the interface level, design level and how they are composed. From its external view, a component consists a set of interfaces, provided to or required from its environment. From its internal view, a component is an executable code that can be coupled with other components via its interfaces. The developer has to ensure that the specification of a component is met by its design and implementation. We also combine component-based and object-oriented techniques in component-based software development This report is a refined version of UNU-IIST Report 276 and is to be presented at and published in the proceedings IFIP WCC-TCS2004, 24-26 August 2004, Toulouse, France.

This book presents thoroughly revised tutorial papers based on lectures given by leading researchers at the International Training School on Domain Modeling and the Duration Calculus, held in Shanghai, China, in September 2007 as an associated event of ICTAC 2007, the 4th International Colloquium on Theoretical Aspects of Computing.The four tutorial papers presented provide competent coverage of software security, domain modeling of software engineering, and duration calculus for real time systems - originating from lectures of leading experts in these fields from Europe and Asia. Topics addressed in detail are: development of real-time systems, domain engineering using abstract modeling, the area of duration calculus, and formal methods like language description using the operational semantics approach.

 This Festschrift volume, published to honour both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays in October and November 2007, includes 25 refereed papers by leading researchers, current and former colleagues, who congregated at a celebratory symposium held in Macao, China, in the course of the International Colloquium on Theoretical Aspects of Computing, ICTAC 2007. The papers cover a broad spectrum of subjects, from foundational and theoretical topics to algorithms and systems issues and to applications, comprising formal methods, systems modelling, hybrid and real-time systems, specification and verification, as well as interval temporal logic.Dines Bjørner is known for his many contributions to the theory and practice of formal methods for software engineering with special focus on abstraction and modelling, specification of systems and languages, and domains, requirements, and software design. He was a professor at the Technical University of Denmark (DTU) in Lyngby, near Copenhagen; he was the founding director of the United Nations University International Institute for Software Technology (UNU-IIST) in Macao during the 1990s; and a co-founder of VDM-Europe, which became Formal Methods Europe, an organisation that promotes the use of formal methods.Zhou Chaochen is known for his seminal contributions to the theory and practice of timed and hybrid systems. Starting at Peking University and as a postgraduate at the Institute for Computing Technology of the Chinese Academy of Sciences, he continued his career with an extended visit to Oxford University Computing Laboratory, where he was the prime instigator of the Duration Calculus, an interval logic for real-time systems. He also worked as a visiting professor at the Technical University of Denmark, Lyngby, at the invitation of Prof. Dines Bjørner. He was a principal research fellow at UNU-IIST during the period 1992-97, before becoming its director, an appointment he held from 1997 to 2002.

This book constitutes the refereed proceedings of the 8th International Conference on Formal Engineering Methods, ICFEM 2006, held in Macao, China, in November 2006.The 38 revised full papers presented together with 3 keynote talks were carefully reviewed and selected from 108 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on specification and verification, internetware and Web-based systems, concurrent, communicating, timing and probabilistic systems, object and component orientation, testing and model checking, tools, fault-tolerance and security, as well as specification and refinement.

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.

We present a mathematical model of class graphs, object graphs and state graphs which naturally capture the essential oo features. A small-step operational semantics of oo programs is defined in the style of classical structural operational semantics, in which an execution step of a command is defined as a transition from one state graph to another obtained by simple operations on graphs. To validate this semantics, we give it an implementation in Java. This implementation can also be used for simulation and validation of oo programs, with the visualization of state graph transitions during the execution. A distinct feature of this semantics is location or address independent. Properties of objects and oo programs can be described as properties of graphs in terms of relations of navigation paths (or attribute strings).

In UML, the general structure of objects, their attributes and relations are modeled as a class graph, and an instance of a class graph is defined as an object graph. The class graph of a system determines the general properties of objects and how objects collaborate in realizing a use case. In this paper, we define class graphs and their object graphs as directed labelled graphs, and investigate in a graph theoretical approach what changes in the object structure maintain the capability of providing services. We define the general notion of structure refinements. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is the resulting class graph should be able to provide at least as well as the original graph. We give a small set of structure refinement rules that is proved to be sound and complete for a kind of structure refinement.

This paper is towards the development of a methodology for object-oriented software development. The intention is to support effective use of a formal model for specifying and reasoning during the requirements analysis and design of a software development process. The overall purpose is to enhance the application of the Unified Modelling Language (UML) with a formal semantics in the Rational Unified Software Development Process (RUP). The semantic framework defines the meaning of some UML submodels. It identifies both the static and dynamic relationships among these submodels. Thus, the focus of this paper is the development of a semantic model to consistently combine a use-case model and a conceptual class diagram to form a system specification.

 This book constitutes the refereed proceedings of the 4th International Colloquium on Theoretical Aspects of Computing, ICTAC 2007 held in Macau, China in September 2007.The 29 revised full papers presented together with 3 invited talks and summaries of 2 tutorials were carefully reviewed and selected from 69 submissions. The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing such as automata theory and formal languages, principles and semantics of programming languages, software architectures and their description languages, software specification, refinement, and verification, model checking and theorem proving, real-time, embedded and hybrid systems, theory of parallel, distributed, and internet-based (grid) computing, simulation and modeling, and service-oriented development.

 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.

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.

We use a formal object-oriented specification language (OOL) to formalize and combine some UML models. With the formalization, we develop a set of refinement laws of UML models that captures the essential nature, principles, nature and patterns of object-oriented design. With the support of the incremental and iterative features of object-orientation and the Rational Unified Process (RUP), our method supports precise and consistent UML model transformation. Keywords: Design patterns, model consistency, model integration, model refinement