Requirements changes can occur both during and after a phase of development for a variety of reasons, including error correction and feature changes. It is difficult and intensive work to integrate requirements changes made after specification is completed. Sequence-based specification was developed to convert ordinary functional software requirements into complete, consistent, and traceably correct specifications through a constructive process. Algorithms for managing requirements changes meet a very great need in field application of the sequence-based specification method. In this paper we propose to capture requirements changes as a series of atomic changes in specifications, and present polynomial-time algorithms for managing these changes. The algorithms are built into the tool support with which users are able to push requirements changes through to changes in specifications, maintain old specifications over time and evolve them into new specifications with the least amount of human interaction and rework. All our change algorithms are supported by rigorous mathematical formulation and proof of correctness. The application example is a safe controller.

The WS-BPEL language has recently become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many recent works have mainly focused on formal semantic models for WS-BPEL. In this paper, we make one step forward by investigating the verification problem for business processes written in BPEL-like languages. We propose a set of proof rules in Hoare-logic style as an axiomatic verification system for a BPEL-like core language containing key features such as data states, fault and compensation handling. We also propose a big-step operational semantics which incorporates all these key features. Our verification rules are proven sound with respect to this underlying semantics. The application of the verification rules is illustrated via the proof search process for a nontrivial example.

The population protocol model has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker. We report our verification results and discuss the issue of modeling strong fairness constraints in Spin.

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.

In this paper we introduce SMoL, a simplified BPEL-like language for specifying peer and service behaviour in P2P systems. We then define a transformational semantics of SMoL in terms of Yet Another Workflow Language (YAWL) workflow

The concept of aspect-orientation allows for modularizing crosscutting concerns as aspect modules. Aspect-orientation originally emerged at the programming level, and has stretched over other development phases now. Among them aspect-oriented modeling (AOM) is a hot topic, and there are many approaches supporting it. Petri net is a good formalism which can provide the foundations for modeling software and simulating its execution, but fails to resolve the problem of crosscutting concerns to support AOM. So, this paper presents an approach which extends the Petri net so as to support the AOM. In this paper, the basic functions of the system are modeled as base net by Petri net, and the crosscutting concerns are modeled as aspect nets. In order to analyze the whole system, woven mechanism is proposed to compose the aspect nets and base net together. The problems about aspect-aspect conflict and conflict relations may exist among the aspect nets matching the shared join point, thus this paper propose solutions to resolve them. The Object Petri net which is an extension of traditional Petri net is also extended so as to support aspect-oriented modeling here.

To express semantic knowledge of natural languages accurately and unify the processing of languages, the style transformation of natural languages is discussed in an all-round way. The discussion covers purpose, voice, modal, tense, narrow sense of style, number and case. All style transformations may be described accurately by a four-element Descriptive Language of Style Transformation (STDL). The transformation between representation of semantic units without style and with style can be converted through style transformation function. Each style transformation function is a difference function in multiple natural languages. Such difference functions can be used to simplify language processing procedure and improve processing quality.

Although the triangle non-symmetry and anti-packing model (TNAM) representation for gray images is an effective image representation method, there is still much space left for optimization. In this paper, inspired by the optimization idea of the packing problem, we proposed an improved algorithm for gray image representation using the non-symmetry and anti-packing model with triangles and rectangles (NAMTR). By comparing the representation algorithm of the NAMTR with those of the TNAM and the popular linear quadtree, theoretical and experimental results presented in this paper show that the former can greatly reduce the number of sub-patterns or nodes and simultaneously save the data storage much more effectively than the latter, and therefore it is a better method to represent gray images. Representation method of the NAMTR, as envisaged in this paper, shows a very strong promise, and it is valuable for further theoretical research and potential business foreground, such as reducing storage space, increasing transmission speed and improving pattern match efficiency.

Most of the state-of-the-art localization algorithms in wireless sensor networks (WSNs) are vulnerable to various kinds of location attacks, whereas secure localization schemes proposed so far are too complex to apply to power constrained WSNs. This paper provides a distributed robust localization algorithm called Bilateration that employs a unified way to deal with all kinds of location attacks as well as other kinds of information distortion caused by node malfunction or abnormal environmental noise. Bilateration directly calculates two candidate positions for every two heard anchors, and then uses the average of a maximum set of close-by candidate positions as the location estimation. The basic idea behind Bilateration is that candidate positions calculated from reasonable (i.e., error bounded) anchor positions and distance measurements tend to be close to each other, whereas candidate positions calculated from false anchor positions or distance measurements are highly unlikely to be close to each other if false information are not collaborated. By using ilateration instead of classical multilateration to compute location estimation, Bilateration requires much lower computational complexity, yet still retains the same localization accuracy. This paper also evaluates and compares Bilateration with three multilateration-based localization algorithms, and the simulation results show that Bilateration achieves the best comprehensive performance and is more suitable to real wireless sensor networks.

The National Knowledge Infrastructure (NKI) is a multi-domain knowledge base. The classical type theory is no longer appropriate to describe every kind of object in multi-domains, such as artifacts, natural or micro objects. Three different kinds of type theories are defined: the classical, atomic and pseudo type theories; in the classical type theory, two new type constructors are defined: setm and ∨, to describe the types of sets of all the elements of the types and unions of two sets of different types, respectively. The structures and categories in the type theory are defined, and the sub-structures and homomorphic structures are used to describe the part-of relations that give the algebraic specifications for the natural objects and the part-of relations between the natural objects, micro objects and artifacts.