Abstract Since the original development of program slicing in 1979 there have been many attempts to define a suitable semantics, which will precisely define the meaning of a slice. Particular issues include handling termination and nontermination, slicing nonterminating programs, and slicing nondeterministic programs. In this paper we review and critique the main attempts to construct a semantics for slicing and present a new operational semantics, which correctly handles slicing for nonterminating and nondeterministic programs. We also present a modified denotational semantics, which we prove to be equivalent to the operational semantics. This provides programmers with 2 different methods to prove the correctness of a slice or a slicing algorithm and means that the program transformation theory and FermaT transformation system, developed last 25 years of research, and which has proved so successful in analyzing terminating programs, can now be applied to nonterminating interactive programs.

Abstract The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate “verification” step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.

Security requirements deal with the protection of assets against unauthorized access (disclosure or modification) and their availability to authorized users. Temporal constraints of history-based access control policies are difficult to express naturally in traditional policy languages. We propose a compositional formal framework for the specification and verification of temporal access control policies for security critical systems in which history-based policies and other temporal constraints can be expressed. In particular, our framework allows for the specification of policies that can change dynamically in response to time or events enabling dynamic reconfiguration of the access control mechanisms. The framework utilizes a single well-defined formalism, interval temporal logic, for defining the semantics of these policies and to reason about them. We illustrate our approach with a detailed case study of an electronic paper submission system showing the compositional verification of their safety, liveness and information flow properties.

This paper proposes a novel fusion technique using iris-online signature biometrics at feature level space. The biometric features are extracted from the pre-processed images of iris and the dynamics of signatures. We propose different fusion schemes at feature level. In order to reduce the complexity of the fusion scheme, we adopt a binary particle swarm optimization (BPSO) procedure which allows the number of features to be significantly reduced while highlighting the difference between classes. This paper examines how the accuracy will be improved as several biometric data are integrated in an identification system. Results show a significant improvement in performance when classification performed at feature fusion level.

In this paper, we present a case study in deriving an algorithm from a formal specification via FermaT transformations. The general method (which is presented in a separate paper) is extended to a method for deriving an implementation of a program transformation from a specification of the program transformation. We use program slicing as an example transformation since this is of interest outside the program transformation community. We develop a formal specification for program slicing in the form of a WSL specification statement which is refined into a simple slicing algorithm by applying a sequence of general purpose program transformations and refinements. Finally, we show how the same methods can be used to derive an algorithm for semantic slicing. The main novel contributions of this paper are: 1) developing a formal specification for slicing, 2) expressing the definition of slicing in terms of a WSL specification statement, and 3) by applying correctness preserving transformations to the specification, we can derive a simple slicing algorithm.

Arabic is widely spoken language but very few text mining tools have been developed for Arabic language. This paper presents an algorithm for automatically building dictionaries. The target domain is crime profiling. The corpus is mined for crime type, location and nationality. This work is then validated through three experiments, the results of which show that the algorithm developed here is promising.

Modern business goals are often fulfilled with workflows that may cross many organisations and utilise services on a variety of devices and/or supported by different platforms. Current workflows are inherently context-aware. Each context is governed and constrained by its own policies and rules to prevent unauthorised participants from executing sensitive tasks and also to prevent tasks from accessing unauthorised services and/or data. We present a context-aware and secure workflow systems together with an efficient agent-based and sound approach for the enforcement of security policies.

Sufficient test coverage for Software Agents that operate in an open and dynamic environment is unlikely to be achieved during the agents' development. Especially when agents exhibit self properties and are constantly adapting to changes in their environment it is important to limit their autonomy to ensure that their behaviour lies within safe boundaries. To increase the trust in the agents, once they are released, we propose to continuously validate/enforce safety properties during their execution. This approach is known as run-time verification and is achieved by inserting assertion points in the agents' codes. The safety properties are expressed as dynamic policies, that can change depending on time or events. The paper shows the flexibility and expressiveness of our policy language to describe temporal constraints on the agents' behaviours. Three conceptually different levels of constraints are investigated. Mechanisms that allow to detect (and possibly recover from) unsafe behaviour are evaluated using a simulated road-network as a case-study.

Abstract One of the most challenging tasks a programmer can face is attempting to analyse and understand a legacy assembler system. Many features of assembler make analysis difficult, and these are the same features that make migration from assembler to a high‐level language difficult. In this paper, we discuss the application of program transformation technology to assist with analysing and understanding legacy assembler systems. We briefly introduce the fundamentals of our program transformation theory and program slicing, which generalizes to conditional semantic slicing. These transformations are applied to a large commercial assembler system to automatically generate high‐level abstract descriptions of the behaviour of each assembler module, with error handling code sliced away. The assembler system was then migrated to C. The result is a dramatic improvement in the understandability of the programs; on average a 6000‐line assembler listing is condensed down to a 132‐line high‐level language abstraction. A second case study, involving over one million lines of source code from many different assembler systems, showed equally dramatic results. Copyright © 2008 John Wiley & Sons, Ltd.

Usage Control (UCON) Models, similar to Access Control Models, control and govern the users' access to resources and services that are available in the system. One of the major improvements of UCON over traditional access control models is the continuity of the control and the concept of attribute mutability. In this paper we provide an alternative formalisation of the UCON model that relaxes many of the assumptions made in earlier formalisations of the model. We question the enforceability of UCON policies as described by previous formalisations and improve on it.

The aim of this article is to provide a unified mathematical framework for program slicing which places all slicing work for sequential programs on a sound theoretical foundation. The main advantage to a mathematical approach is that it is not tied to a particular representation. In fact the mathematics provides a sound basis for any particular representation. We use the WSL (wide-spectrum language) program transformation theory as our framework. Within this framework we define a new semantic relation, semirefinement , which lies between semantic equivalence and semantic refinement. Combining this semantic relation, a syntactic relation (called reduction ), and WSL's remove statement, we can give mathematical definitions for backwards slicing, conditioned slicing, static and dynamic slicing, and semantic slicing as program transformations in the WSL transformation theory. A novel technique of “encoding” operational semantics within a denotational semantics allows the framework to handle “operational slicing”. The theory also enables the concept of slicing to be applied to nondeterministic programs. These transformations are implemented in the industry-strength FermaT transformation system.

A Service oriented system emerges from composition of services. Dynamically composed reactive Web services form a special class of service oriented system, where the delays associated with communication, unreliability and unavailability of services, and competition for resources from multiple service requesters are dominant concerns. As complexity of services increase, an abstract design language for the specification of services and interaction between them is desired. In this paper, we present ASDL (Abstract Service Design Language), a wide spectrum language for modelling Web services. We initially provide an informal description of our computational model for service oriented systems. We then present ASDL along with its specification oriented semantics defined in Interval Temporal Logic (ITL): a sound formalism for specifying and reasoning about temporal properties of systems. The objective of ASDL is to provide a notation for the design of service composition and interaction protocols at an abstract level.

A program transformation is an operation which can be applied to any program (satisfying the transformations applicability conditions) and returns a semantically equivalent program. In the FermaT transformation system program transformations are carried out in a wide spectrum language, called WSL, and the transformations themselves are written in an extension of WSL called MetaWSL which was specifically designed to be a domain-specific language for writing program transformations. As a result, FermaT is capable of transforming its own source code via meta-transformations. This paper introduces MetaWSL and describes some applications of meta-transformations in the FermaT system.

We describe the legacy assembler problem and describe how the FermaT transformation system is used to reengineer assembler systems and migrate from assembler to C and COBOL.

Current ontological specifications for semantically describing properties of Web services are limited to their static interface description. Normally for proving properties of service compositions, mapping input/output parameters and specifying the pre/post conditions are found to be sufficient. However these properties are assertions only on the initial and final states of the service respectively. They do not help in specifying/verifying ongoing behaviour of an individual service or a composed system. We propose a framework for enriching semantic service descriptions with two compositional assertions: assumption and commitment that facilitate reasoning about service composition and verification of their integration. The technique is based on Interval Temporal Logic(ITL): a sound formalism for specifying and proving temporal properties of systems. Our approach utilizes the recently proposed Semantic Web Rule Language.

The maintenance and evolution of distributed, heterogeneous software components; including both legacy and green-field subsystems is described through a highly re-configurable architectural style. It is shown how this architectural style is realized through identification, separation and externalization of a formal specification of the manners of the application domain and its components. The approach is based on the notion of enterprise component (EC). An enterprise component is defined as an architectural pattern that is leveraged to provide a uniform mechanism for management of component boundaries between otherwise entropic systems consisting of multiple legacy systems coexisting with newer, object and component-based application programs. EC's are identified through a domain decomposition that includes mapping business architecture onto component-based software architecture. Extensions to current methodologies and architectural practices to support and realize such a style are presented.

Business processes and goals change rapidly due to the turbulent environment in which they operate. Their supporting and underpinning technologies may, as a result, require to change. Meanwhile, technological advances are being made at an increasing rate. This may trigger changes in business goals and processes to exploit these new advances; a notable example is e-commerce and e-learning. Understanding and analyzing the interplay and the dual effect between these two entities, technologies and business, is vital both for the prosperity of business and the success and further development of the technologies themselves. This paper proposes the K-Mediator framework together with its underpinning theory to facilitate the co-evolution between businesses and their supporting technologies.

This paper advocates that extracting formal specification semantically consistent to the original legacy system will facilitate further redesign and forward engineering greatly. The three parts of reengineering could be integrated on the basis of a wide spectrum language. The key approach to comprehension and the production of formal specification is a notion of abstraction. Transformation can help to change the original source code into alternative forms, but with the same semantics. Abstraction is often interpreted as the act of hiding irrelevant details. What constitute as relevant details is often left open to different interpretations. A unified approach for reverse engineering is described within which the notion of abstraction is classified and precisely defined. Abstraction rules are given and applied to various case studies. Copyright © 2000 John Wiley & Sons, Ltd.

We propose a sound and practical approach, based on a formal method (known as interval temporal logic), to cope with 'change' and analyse its effect. The approach allows lows to capture a snapshot of system's behaviour over which various interesting properties, such as liveness, timeliness and safety properties, can be validated compositionally. These properties may include invariants that are required to be valid after changes have taken place. We also present and evaluate the design and implementation of a formal tool, AnaTempura, which supports the developed approach. A case study is presented to illustrate our approach and the tool.

We present a calculus which can transfer specifications to objects for the development of real-time systems. The object model is based on a practical OO development technique-HRT-HOOD. A real-time logic is specified by extending a sound formal method for real-time systems-TAM, to formalise the object model. With integration of HRT-HOOD and TAM, the advantages of object-oriented structured methods with the stepwise refinement techniques are combined. The result is illustrated on a case study.

It is widely accepted that reverse engineering has three components: restructuring, comprehension and production of formal specification. In this paper, we advocate that the three components could be achieved in a systematic approach by successfully applying a series of sound rules. The key approach to comprehension and the production of formal specification is a notion of abstraction. Abstraction is often interpreted as the act of hiding irrelevant details. What constitute as relevant details is often left open to different interpretations. A unified approach for reverse engineering is described within which the notion of abstraction is classified and precisely defined. Abstraction rules are given and applied to various small examples.

Discusses the current situation of formal methods and their use in the re-engineering of computing systems, especially real-time systems. Based on the analysis results, a solution which uses a consistent 4-sector Wide Spectrum Language (WSL) is proposed, which presently includes the general architecture and work flow, the structure of the Object-Action Model, the syntax and semantics of the Object-oriented Temporal Agent Model (ObTAM) and the Timed Guarded Command Language (TGCL). A small case study shows an optimistic future for our WSL technique. Further research will aim to build the complete semantic kernel of the WSL and its associated algebraic laws, including transformation rules and abstraction rules.

This paper presents a short review of formal methods and their use in the re-engineering of computing systems. Five classes of formal notations and theories, namely state/model-based, logic-based, algebraic-based, process algebra and net-based formalisms together with combined formalisms are considered, analyzed and compared. Conclusions obtained focus on proposing an approach to building a practical re-engineering system.

We describe the Temporal Agent Model (TAM) together with its associated refinement calculus. The calculus is based on a wide-spectrum language within which functional and temporal properties can be expressed in either abstract (i.e. specification) or concrete (i.e. design) terms. The refinement process transforms abstract specifications to concrete designs through successive applications of sound refinement laws. An extension to the calculus allows us to calculate a scheduler for the resulting design. We present a specification paradigm based on splitting the functional and temporal requirements, and describe refinement techniques based on this paradigm. We illustrate the calculus with an example taken from the avionics industry.