Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.

As a variety of digital services are provided through networks, more and more efforts are made to ensure dependability of software behavior implementing services. Formal methods and tools have been considered as promising means to support dependability in complex software systems during the development. On the other hand, there have been serious doubts on practical applicability of formal methods. This paper overviews the present state of formal methods and discusses their applicability, especially focusing on two representative methods (SPIN and B Method) and their recent industrial applications. This paper also discusses applications of formal methods to dependable networked software.

Recommender System (RS) predicts user's ratings towards items, and then recommends highly-predicted items to user. In recent years, RS has been playing more and more important role in the agent research field. There have been a great deal of researches trying to apply agent technology to RS. Collaborative Filtering, one of the most widely used approach to predict user's ratings in Recommender System, predicts a user's rating towards an item by aggregating ratings given by users who have similar preference to that user. In existing approaches, user similarity is often computed on the whole set of items. However, because the number of items is often very large and so is the diversity among items, users who have similar preference in one category may have totally different judgement on items of another kind. In order to deal with this problem, we propose a method to cluster items, so that inside a cluster, similarity between users does not change significantly from item to item. After the item clustering phase, when predicting rating of a user towards an item, we only aggregate ratings of users who have similarity preference to that user inside the cluster of that item. Experiments evaluating our approach are carried out on the real dataset taken from MovieLens, a movies recommendation web site. Experiment results suggest that our approach can improve prediction accuracy compared to existing approaches.

Test coverage is an important indicator of whether software has been sufficiently tested. However, there are several problems with the existing measurement tools for test coverage, such as their cost of development and maintenance, inconsistency, and inflexibility in measurement. We propose a consistent and flexible measurement framework for test coverage that we call the Open Code Coverage Framework (OCCF). It supports multiple programming languages by extracting the commonalities from multiple programming languages using an abstract syntax tree to help in the development of the measurement tools for the test coverage of new programming languages. OCCF allows users to add programming language support independently of the test-coverage-criteria and also to add test-coverage-criteria support independently of programming languages in order to take consistent measurements in each programming language. Moreover, OCCF provides two methods for changin the measurement range and elements using XPath and adding user code in order to make more flexible measurements. We implemented a sample tool for C, Java, and Python using OCCF. OCCF can measure four test-coverage-criteria. We also confirmed that OCCF can support C#, Ruby, JavaScript, and Lua. Moreover, we reduced the lines of code (LOCs) required to implement measurement tools for test coverage by approximately 90% and the time to implement a new test-coverage-criterion by over 80% in an experiment that compared OCCF with the conventional non-framework-based tools.