山本 光晴

Apache ZooKeeper is a distributed data storage that is highly concurrent and asynchronous due to network communication; testing such a system is very challenging. Our solution using the tool "Modbat" generates test cases for concurrent client sessions, and processes results from synchronous and asynchronous callbacks. We use an embedded model checker to compute the test oracle for non-deterministic outcomes; the oracle model evolves dynamically with each new test step. Our work has detected multiple previously unknown defects in ZooKeeper. Finally, a thorough coverage evaluation of the core classes show how code and branch coverage strongly relate to feature coverage in the model, and hence modeling effort.

Karp-Miller tree construction on Petri nets is a classical well-known algorithm to construct the minimal coverability set via forward analysis. It enables us to construct decision procedures for several problems such as coverability and (place) boundedness. This paper formalizes Karp-Miller tree construction on Petri nets, and its correctness with respect to coverability using COQ and Ss REFLECT. Instead of showing soundness and completeness for trees directly, we prove these properties for transition systems derived from Petri nets, and then relate them with trees so we can make use of well-established libraries and also avoid making proofs complicated. Termination of the tree construction is guaranteed by defining it as a COQ function with a well-foundedness proof. Although the termination proof for Karp-Miller tree is usually made with classical reasoning, we avoided it so the whole formalization can be done in an axiom-free way with respect the default COQ theory. This work will provide us with a basis for further formalization of several optimized algorithms, some of which are known to be error prone, and also a template for Karp-Miller style algorithms on extended variants of Petri nets.

Many text mining tools cannot be applied directly to documents available on web pages. There are tools for fetching and preprocessing of textual data, but combining them in one working tool chain can be time consuming. The preprocessing task is even more labor-intensive if documents are located on multiple remote sources with different storage formats. In this paper we propose the simplification of data preparation process for cases when data come from wide range of web resources. We developed an open-sourced tool, called Kayur, that greatly minimizes time and effort required for routine data preprocessing steps, allowing to quickly proceed to the main task of data analysis. The datasets generated by the tool are ready to be loaded into a data mining workbench, such as WEKA or Carrot2, to perform classification, feature prediction, and other data mining tasks.