Exception handling is a mechanism in modern programming languages. Studies have shown that the exception handling code is error-prone. However, there is still limited research on detecting exception handling bugs, especially for C++ programs. To tackle the issue, we try to precisely represent the exception control flow in C++ programs and propose an analysis method that makes use of the control flow to detect such bugs. More specifically, we first extend control flow graph by introducing the concepts of five different kinds of basic blocks, and then modify the classic symbolic execution framework by extending the program state to a quadruple and properly processing try, throw and catch statements. Based on the above techniques, we develop a static analysis tool on the top of Clang Static Analyzer to detect exception handling bugs. We run our tool on projects with high stars from GitHub and find 36 exception handling bugs in 8 projects, with a precision of 84%. We compare our tool with four state-of-the-art static analysis tools (Cppcheck, Clang Static Analyzer, Facebook Infer and IKOS) on projects from GitHub and handmade benchmarks. On the GitHub projects, other tools are not able to detect any exception handling bugs found by our tool. On the handmade benchmarks, our tool has a significant higher recall.

The smart pointer mechanism, which is improved in the continuous versions of the C++ standards over the last decade, is designed to prevent memory-leak bugs by automatically deallocating the managed memory blocks. However, not all kinds of memory errors can be immunized by adopting this mechanism. For example, dereferencing a null smart pointer will lead to a software failure. Due to the lack of specialized support for smart pointers, the off-the-shelf C++ static analyzers cannot effectively reveal these bugs.In this paper, we propose a static approach to detecting memory-related bugs by tracking the heap memory management of smart pointers. The behaviors of smart pointers are modeled during their lifetime to trace the state transitions of managed memory blocks. And the specially designed checkers are used to check the state changes according to five collected bug patterns. To evaluate the effectiveness of our approach, we implement it on the top of the Clang Static Analyzer. A set of handmade code snippets, as well as nine popular open-source C++ projects, are used to compare our tool against four other analyzers. The results show that our approach can successfully discover nearly all the built-in bugs. And 442 out of 648 reports generated from the open-source projects are true positives after manual reviewing, where the bugs of dereferencing null smart pointers are most frequently reported. To further confirm our reports, we design patches for Aria2, Restbed, MySQL and LLVM, in which seven pull requests covering 76 bug reports have been merged by the developers up to now. The results indicate that pointers should always be carefully used even after migrated to smart pointers and static analysis upon specialized models can effectively detect such bugs.

Correct mutual-exclusion is one of the key challenges in concurrent programming. Although the fine-grained locking schema can be more efficient compared with the coarse-grained techniques, it is tough to use, as well as error-prone. Here we present a static approach, based on program analysis, to automatically add fine-grained locking primitives to data structures implemented as classes. For tree-like structures, the modified class definitions are guaranteed to be thread-safe. Experiments show that the approach can successfully deal with programs which are challenging to be handled manually, and it works efficiently.

Algebraic specification is well-known in specifyingabstract data types. It could also play an important role inverifying the interrelation between methods in classes. In thispaper we develop a framework for verifying the conformanceof method implementations against an algebraic specification. Different from most existing work that perform testing atthe code level for the conformance, our approach verifies theconformance without touching the implementation details. Asanother contribution, we show that if all the inherited methods ofa subclass satisfy behavioral subtyping, then the subclass conformsto the algebraic specification of its superclass, i.e., there is no needto re-verify.

Summary Grammar‐based test generation provides a systematic approach to producing test cases from a given context‐free grammar. Unfortunately, naive grammar‐based test generation is problematic because of the fact that exhaustive random test case production is often explosive, and grammar‐based test generation with explicit annotation controls often causes unbalanced testing coverage. In this paper, we present an automatic grammar‐based test generation approach, which takes a symbolic grammar as input, requires zero control input from users, and produces well‐distributed test cases. Our approach utilizes a novel dynamic stochastic model where each variable is associated with a tuple of probability distributions, which are dynamically adjusted along the derivation. We further present a coverage tree illustrating the distribution of generated test cases and their detailed derivations. More importantly, the coverage tree supports various implicit derivation control mechanisms. We implemented this approach in a Java‐based system, namedGena. Each test case generated byGenaautomatically comes with a set of structural features, which can play an important and effective role on automated failure causes localization. Experimental results demonstrate the effectiveness of our approach, the well‐balanced distribution of generated test cases over grammatical structures, and a case study on grammar‐based failure causes localization. Copyright © 2014 John Wiley & Sons, Ltd.

Verification of concurrent systems is difficult because of their inherent nondeterminism. Modern verification requires clean specifications of inter-thread interferences and modular reasoning over separated components. But for message-passing models, a general reasoning system, which meets these standards, is still in demand. Here we propose a new logic for verifying distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and constrain the environmental interferences by logical invariants. The verification is compositional w.r.t. agents as long as some inter-agent constraints are satisfied. Using this logic we successfully verified two classic message-passing algorithms: leader election and merging network.

Web services choreography describes the global model of service interactions among a set of participants. In order to achieve a common business goal, the protocols for interactions must be correct. Experiences show that it is difficult to check choreography manually, even it is not very complex. A scenario describes a sequence of interactions among the collaborative participants, that is useful for judging if a choreography satisfies the intended business requirements. However, building the scenarios for a choreography is not easy even if with a supporting tool, such as Pi4SOA. In this paper, we propose an approach, and a set of algorithms, for generating the scenarios of a choreography automatically. For the fundamental study, a small choreography language CDL capturing the core features of Web services choreography description language WS-CDL is developed, with its formal syntax and trace semantics. The scenarios are defined basing on the choreography model, and the algorithms for generating scenarios from CDL is presented. We use a purchase order example to show how service choreography can be specified in CDL, and how the scenarios are generated and used to check the choreography. A prototype tool has been developed on Pi4SOA which shows the approach is both viable and effective.

WS-BPEL has emerged as the de facto industry standard for composing Web services. With the wide attention for WS-BPEL, Quality of Service (QoS) for it has become a key differentiator to judge the services with same functionalities. One main challenge currently is how to analyze the QoS of WS-BPEL services at the early design phase. This work aims at proposing a methodology for model-based analysis of WS-BPEL processes, with a focus on the assessment of non-functional quality attributes. Particularly, we define a small language BPELR to model the core features of WS-BPEL language, and annotate message receiving and service invoking activities with message-arrive rate and service-execute rate separately. Then a set of rules are proposed for translating BPELR into the input language of the probabilistic model checker PRISM, which can be used to stochastically analyze WS-BPEL processes. Finally, we show our approach by a purchase order business process example.

Specification and verification for object oriented (OO) programs remains a great challenge despite of decades' efforts. To address the problem, we propose a novel specification and verification framework, which supports abstraction and offers modularity via a set of scope and inheritance rules, and a concept called\emph{specification predicate}. The framework covers the most important OO features like encapsulation, inheritance and polymorphism, while only one specification per method is necessary. It can successfully deal with inheritance, keep still modularity in verification, and avoid re-verification of the implementation. We show how the framework can be integrated into an OO language, and use examples to illustrate how the specification and verification can be carried out in our framework following the structures of OO programs in an abstract and modular way.

JavaScript as a Web scripting language has been widely used following the fast growth of Internet. Due to the flexible and dynamic features offered by the JavaScript language, it has become a challenging problem to statically reason about code written in JavaScript. As a first step towards building a mechanised verification system for JavaScript, we present, in this paper, an axiomatic verification system for a core subset of JavaScript based on a variant of separation logic. We have also defined a big-step operational semantics with respect to which we have demonstrated the soundness of our verification system.

Ubiquitous embedded systems are often resource-constrained. Developing software for these systems should take into account resources such as memory space. In this paper, we develop and implement an analysis framework to infer statically stack usage bounds for assembly-level programs in abstract Java Byte code. Our stack bound inference process, extended from a theoretical framework proposed earlier by some of the authors, is composed of deductive inference rules in multiple passes. Based on these rules, a usable tool has been developed for processing programs to capture the stack memory needs of each procedure in terms of the symbolic values of its parameters. The final result contains path-sensitive information to achieve better precision. The tool invokes a Presburger solver to perform fixed point analysis for loops and recursive procedures. Our initial experiments have confirmed the viability and power of the approach.

We introduce a tool under development for assembly-level programs, which captures memory requirement of each method in terms of symbolic values of its parameters. It exploits fix-point analysis for loops and recursions. Up now the tool can handle most common structures in programs except some rare situations.

Artifact-centric business process models allow to describe artifacts (data objects) and their life cycles, which allow designers to focus on individual artifact in business processes, thus simplifies the design and analysis of business process model. However, this feature is a double-edged sword. The description of the relationships between artifacts becomes a new and nontrivial problem. It is better that the associations among business artifacts are specified at a high level as logical assertions. We think taking business constraints as complements of artifact-centric business operational model is an useful idea. Based on this consideration,in this paper, we propose an approach which combines both the declarative way and the procedural way in the construction of business processes. This flexibility can help designers to separate the parts of a business process that are more likely to change from those that are less likely to change. We propose a language TiLE to specify business constraints, and give complexity results on the satisfiability of TiLE. Moreover, we discussed how to enforce the constraints at run-time.

Abstract An object-oriented program consists of a section of class declarations and a main method . The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications. With a UML-like modeling language, the class declaration section of a program is represented as a class diagram , and the instances of the class diagram are represented by object diagrams , that form the state space of the program. In this paper, we define a class diagram and its object diagrams as directed labeled graphs , and investigate what changes in the class structure maintain the capability of providing functionalities (or services ). We formalize such a structure change by the notion of structure refinement . 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 many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement , as an extension to the classical theory of data refinement , in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation.

Channel passing mechanisms enable dynamically determining destinations of message transferring. WS-CDL, a language developed by W3C for the specification of Web services choreographies, adopts channel passing to support dynamic Web services composition. A choreography can be projected into individual services or orchestration skeletons. It is a challenge to ensure the services generated from a choreography always have sufficient and correct channels to complete their collaboration. In fact, WS-CDL is not ready for rigorous validation and implementation with respect to channel passing, since it provides no structure for specifying explicitly which role should firstly initialize which channel variable. Here we propose an algorithm to uncover these implicit assumptions, that is implemented as an extension to Pi4SOA. With the help of the algorithm, some existing methods for verification and implementation can be applied on choreographies written in WS-CDL. In addition, we propose an approach to detect design defects in choreographies, and show how a defect is found from the main sample choreography in WS-CDL Primer. It seems that choreographies with channel passing are error prone. Methods and tools are necessary to support designers in this field. Also, we suggest improving the situation by adding a syntactical construct to WS-CDL.

BPEL (Business Process Execution Language) has become the standard for specifying and executing workflow specifications for Web service composition invocation. A major weakness of BPEL is the lack of so-called "human workflow" support. The BPEL4People specification tries to amend this by adding human task support to BPEL. In this paper, we propose a formal model of BPEL4People using the CSP process algebra, and discuss some issues we found through analyzing the model. Although based on BPEL4People, this is a general work, and can also be viewed as a formal model of human workflow.

The WS-BPEL language has 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 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.

Confinement of objects is crucial to protect sensitive object references. However, static confinement schemes proposed so far have quite rigorous syntactic restrictions, and also, no similarity in concepts makes assessing of them a difficulty. In this paper, we present a generic framework for reasoning about confinement based on three parts: program states, partition for heaps and the confinement constraints. Particularly, the partition is made according to the system's requirement, whose flexibility leads to the generality of the model. A range of confinement schemes can be characterized in terms of their underlying partition for the heap in our model. As an illustration, we have encoded both confined types and ownership types, and proved the soundness of their type systems in our model that well typed programs are well confined under our formal definition.

Web services choreography describes global models of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel(s) used in the interaction, otherwise the execution will get stuck. Because of dynamic composition, the initial channel set on each participant is often insufficient to meet the requirements. It is the responsibility of the participants to pass required channels owned (known) by one to some others. Since a choreography may involve many participants and complex channel constraints, it is hard for designers to specify channel passing in a choreography exactly as required. In this paper, we address the problem of checking whether a choreography lacks channels or has redundant channels, and how to automatically generate channel passing based on interaction flows of the choreography in the case of channel absence. Concretely, we propose a small language Chorcnamed for a channel interaction sub-language for modeling the channel passing aspect of choreography. Based on the formal operational semantics of Chorc, the algorithms for static checking choreography and generating channel passing are studied as well.

Design patterns capture expert design experience in generic design structure and behavior. A design pattern needs to be instantiated before using. It can be integrated with other patterns as well. The instantiation and integration operations are two important operations when a designer uses a design pattern in a particular application. In this paper, we investigate the commutability of these two operations based on our formal specification framework. We provide rigorous proofs on the conditions when the order of these two operations does not matter. Our results enable the software designers to choose their design processes with assurance of their equivalence.

With the growth of interest on the web services, people pay increasinglyattention to the choreography, that is, to describe collaborations ofparticipants in accomplishing a common business goal from a globalviewpoint. In this paper, based on a simple choreography language and arole-oriented process language, we study some fundamental issues relatedto choreography, especially those related to implementation, includingsemantics, projection and natural projection, dominant role in choices anditerations, etc. We propose the concept of dominant role and somenovel languages structures related to it. The study reveals some cluesabout the language, the semantics, the specification and theimplementation of choreography.

We propose a language CDL as a formal model of simplified WS-CDL. The operational semantics of CDL is given, and static validation and verification of choreographies is studied. Some properties of the proposed model are verified using the SPIN model-checker, which illustrates the potential usage and benefits of the formal model

In the paper, we proposed a language called BPEL0 with its formal semantics as the foundations of WSBPEL. In this paper, we follow the way Van der Aalst proposed on pattern analysis in workflow languages (2003), and present the patterns for BPEL0. Moreover, the expressiveness of BPEL0 is also embodied by means of putting these patterns in the program environment composed of other programming operators. Those properties about the patterns with its environment are captured by the algebraic laws, which can be proven in the framework of BPEL0 semantic domain.

Abstract Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for a synchronous communication model including multiple hardware devices. We transform the partitioning into a reachability problem of timed automata. By means of an optimal reachability algorithm, the optimal solution can be obtained with limited resources in hardware. To relax the initial condition of the partitioning for optimization, two algorithms are designed to explore the dependency relations among processes in the sequential specification. Moreover, we propose a scheduling algorithm to improve the synchronous communication efficiency further after partitioning stage. Some experiments are conducted with the model checker UPPAAL to show our approach is both effective and efficient.