The use of mathematics for documenting, inspecting, and testing software is explained and illustrated. Three measures of software quality are described and discussed. Then three distinct complementary approaches to software quality assurance are presented. A case study, the testing and inspection of a safety-critical system, is discussed in detail.

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.

Meta-modelling plays an important role in model driven software development. In this paper, a graphic extension of BNF (GEBNF) is proposed to define the abstract syntax of graphic modelling languages. From a GEBNF syntax definition, a formal predicate logic language can be induced so that meta-modelling can be performed formally by specifying a predicate on the domain of syntactically valid models. In this paper, we investigate the theoretical foundation of this meta-modelling approach. We formally define the semantics of GEBNF and its induced predicate logic languages, then apply Goguen and Burstall’s institution theory to prove that they form a sound and valid formal specification language for meta-modelling.

Security protocols play more and more important roles with wide use in many applications nowadays. Currently, there are many tools for specifying and verifying security protocols such as Casper/FDR, ProVerif, or AVISPA. In these tools, the intruder’s ability, which either needs to be specified explicitly or set by default, is not flexible in some circumstances. Moreover, whereas most of the existing tools focus on secrecy and authentication properties, few supports privacy properties like anonymity, receipt freeness, and coercion resistance, which are crucial in many applications such as in electronic voting systems or anonymous online transactions.

In this paper, we introduce a framework for specifying security protocols in the labeled transition system (LTS) semantics model, which embeds the knowledge of the participants and parameterizes the ability of an attacker. Using this model, we give the formal definitions for three types of privacy properties based on trace equivalence and knowledge reasoning. The formal definitions for some other security properties, such as secrecy and authentication, are introduced under this framework, and the verification algorithms are also given. The results of this paper are embodied in the implementation of a SeVe module in a process analysis toolkit (PAT) model checker, which supports specifying, simulating, and verifying security protocols. The experimental results show that a SeVe module is capable of verifying many types of security protocols and complements the state-of-the-art security verifiers in several aspects. Moreover, it also proves the ability in building an automatic verifier for security protocols related to privacy type, which are mostly verified by hand now.

Microblogging provides a new platform for communicating and sharing information amongWeb users. Users can express opinions and record daily life using microblogs. Microblogs that are posted by users indicate their interests to some extent. We aim to mine user interests via keyword extraction from microblogs. Traditional keyword extraction methods are usually designed for formal documents such as news articles or scientific papers. Messages posted by microblogging users, however, are usually noisy and full of new words, which is a challenge for keyword extraction. In this paper, we combine a translation-based method with a frequency-based method for keyword extraction. In our experiments, we extract keywords for microblog users from the largest microblogging website in China, Sina Weibo. The results show that our method can identify users’ interests accurately and efficiently.

Social media websites allow users to exchange short texts such as tweets via microblogs and user status in friendship networks. Their limited length, pervasive abbreviations, and coined acronyms and words exacerbate the problems of synonymy and polysemy, and bring about new challenges to data mining applications such as text clustering and classification. To address these issues, we dissect some potential causes and devise an efficient approach that enriches data representation by employing machine translation to increase the number of features from different languages. Then we propose a novel framework which performs multi-language knowledge integration and feature reduction simultaneously through matrix factorization techniques. The proposed approach is evaluated extensively in terms of effectiveness on two social media datasets from Facebook and Twitter. With its significant performance improvement, we further investigate potential factors that contribute to the improved performance.

Group behavior forecasting is an emergent research and application field in social computing. Most of the existing group behavior forecasting methods have heavily relied on structured data which is usually hard to obtain. To ease the heavy reliance on structured data, in this paper, we propose a computational approach based on the recognition of multiple plans/intentions underlying group behavior.We further conduct human experiment to empirically evaluate the effectiveness of our proposed approach.

This paper investigates human mobility patterns in an urban taxi transportation system. This work focuses on predicting humanmobility fromdiscovering patterns of in the number of passenger pick-ups quantity (PUQ) from urban hotspots. This paper proposes an improved ARIMA based prediction method to forecast the spatial-temporal variation of passengers in a hotspot. Evaluation with a large-scale realworld data set of 4 000 taxis’ GPS traces over one year shows a prediction error of only 5.8%. We also explore the application of the prediction approach to help drivers find their next passengers. The simulation results using historical real-world data demonstrate that, with our guidance, drivers can reduce the time taken and distance travelled, to find their next passenger, by 37.1% and 6.4%, respectively.

The field of social computing emerged more than ten years ago. During the last decade, researchers from a variety of disciplines have been closely collaborating to boost the growth of social computing research. This paper aims at identifying key researchers and institutions, and examining the collaboration patterns in the field. We employ co-authorship network analysis at different levels to study the bibliographic information of 6 543 publications in social computing from 1998 to 2011. This paper gives a snapshot of the current research in social computing and can provide an initial guidance to new researchers in social computing.