An assume-guarantee verification method has been recognized as a promising approach to verify component-based software by model checking. This method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. The method allows us to decompose a verification target into components so that we can model check each of them separately. In this method, assumptions are seen as the environments needed for the components to satisfy a property and for the rest of the system to be satisfied. The number of states of the assumptions should be minimized because the computational cost of model checking is influenced by that number. Thus, we propose a method for generating minimal assumptions for the assume-guarantee verification of component-based software. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. We have implemented a tool for generating the minimal assumptions. Experimental results are also presented and discussed.

Ordered attribute grammars (OAGs for short) are a useful class of attribute grammars (AGs). For some attribute grammars, even though they are not circular, OAG circularity test reports that they are not ordered and fails to generate attribute evaluators because some approximation introduces circularities (called type 3 circularities in this paper). First we discuss that it is sometimes difficult for programmers to eliminate type 3 circularities by hand. Second, to reduce this difficulty, we propose a new AG class called OAG* that produces less type 3 circularities than OAG while preserving the positive characteristic of OAG. OAG* uses a global dependency graph GDS that provides a new approximation algorithm. We obtained good results with our experimental implementation of OAG*. It is shown that OAG* is different from the existing GAG and Eli/Liga systems. Finally, two combinations of Eli/Liga and OAG* are provided.

We present a novel replication technique for parallel applications where instances of the replicated application are active on different group of processors called replicas. The replication technique is based on the FTAG (Fault Tolerant Attribute Grammar) computation model. FTAG is a functional and attribute based model. The developed replication technique implements "active parallel replication," that is, all replicas are active and compute concurrently a different piece of the application parallel code. In our model replicas cooperate not only to detect and mask failures but also to perform parallel computation. The replication mechanisms are supported by FTAG run time system and are fully application-transparent. Different novel mechanisms for checkpointing and recovery are developed. In our model during rollback recovery only that part of the computation that was detected faulty is discarded. The replication technique takes full advantage of parallel computing to reduce overall computation time.

This paper proposes a framework for modular verification of evolving component-based software. This framework includes two stages: modular conformance testing for updating inaccurate models of the evolved components and modular verification for evolving component-based software. When a component is evolved after adapting some refinements, the proposed framework focuses on this component and its model in order to update the model and recheck the whole evolved system. The framework also reuses the previous verification results and the previous models of the evolved components to reduce the number of steps required in the model update and modular verification processes. An implementation and some experimental results are presented.

The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. However, the computational cost for generating the minimal assumption is very high so the method is difficult to be applied in practice. This paper presents an optimization as a continuous work of the minimized assumption generation method in order to reduce the complexity of the method. The key idea of this method is to find a smaller assumption in a sub-tree of the search tree containing the candidate assumptions using the depth-limited search strategy. With this approach, the improved method can generate assumptions with a lower computational cost and consumption memory than the minimized method. The generated assumptions are also effective for rechecking the systems at much lower computational cost in the context of software evolution. An implemented tool supporting the improved method and experimental results are also presented and discussed.

In this paper, we introduce an approach of service adaptation for behavior mismatching services using pushdown model checking. This approach uses pushdown systems as model of adaptors so that capturing non-regular behavior in service interactions is possible. Also, the use of pushdown model checking integrates adaptation and verification. This guarantees that an adaptor generated by our approach not only solves behavior mismatches but also satisfies usual verification properties if specified. Unlike conventional approaches, we do not count on specifications of adaptor contracts but take only information from behavior interfaces of services and perform fully automated adaptor generation. Three requirements relating to behavior mismatches, unbounded messages, and branchings are retrieved from behavior interfaces and used to build LTL properties for pushdown model checking. Properties for unbounded messages, i.e., messages sent and received arbitrary multiple times, are especially addressed since it characterizes non-regular behavior in service composition. This paper also shows some experimental results from a prototype tool and provides directions for building BPEL adaptors from behavior interface of generated adaptor. The results show that our approach does solve behavior mismatches and successfully capture non-regular behavior in service composition under the scale of real service applications.

We have launched "Highly-Reliable Embedded Software Development" Project, held as a part of e-Society Project, supported by Ministry of Education, Culture, Sports, Science and Technology (MEXT), Japan. The aim of this project is to enable the industry to produce highly reliable and advanced software by introducing latest software technologies into embedded software development. In this paper, we introduce the overview of the projects and our activities and results so far.