Yojiro Harie

Model checking is a fundamental technique for verifying finite state concurrent systems. Traditionally, model designs were initially created to facilitate the application of model checking. This process, representative of Model Driven Development (MDD), involves generating an equivalent code from a given model which is verified before implementation begins. However, this approach is considerably slower compared to agile development methods and lacks flexibility in terms of expandability and refactoring. We have proposed "CodoMo: Python Code to Model Generator for pyModelChecking." This tool automates the transformation of a Python code by an AST static analyzer and a concolic testing tool into intermediate models suitable for verification with pyModelChecking, bridging the gap between traditional model checking and agile methodologies. Additionally, we have implemented a multiprocess approach that integrates the execution of PyExZ3 with the generation of Kripke structures achieving greater work efficiency. By employing CodoMo, we successfully verified a Tello Drone programming with gesture-based image processing interfaces, showcasing the tool's powerful capability to enhance verification processes while maintaining the agility required for today's fast-paced development cycles.

Growth prediction technology is not only a practical application but also a crucial approach that strengthens the safety of image processing techniques. By supplementing the growth images obtained from the original images, especially in insufficient data sets, we can increase the robustness of machine learning. Therefore, predicting the growth of living organisms is an important technology that increases the safety of existing applications that target living organisms and can extend to areas not yet realized. This paper is a systematic literature review (SLR) investigating biological growth prediction based on the PRISMA 2020 guidelines. We systematically survey existing studies from 2017 to 2022 to provide other researchers with current trends. We searched four digital libraries—IEEE Xplore, ACM Digital Library, Science Direct, and Web of Science—and finally analyzed 47 articles. We summarize the methods used, year, features, accuracy, and dataset of each paper. In particular, we explained LSTM, GAN, and STN, the most frequently used methods among the 20 papers related to machine learning (40% of all papers).

Wild Deer’s grazing in farmers and villager’s field has caused serious troubles for the residents and concerned authorities here in Northern Hokkaido of Japan. Furthermore, the number of deer in northern Japan is increasing rapidly leading to increment in road accidents which is also becoming a serious problem that needs to be handled. Several procedures have been followed to avoid or at least minimize the destruction caused by the white-tailed deer, but a solid solution is yet to be found. To this context, we are proposing a highly effective solutions to identify the individual wild deer and pinpoint the most trouble causing group of deer’s using augmented triplet network, a novel technique of computer vision. Initially the deer are recognized and classified individually which will help us track the deer and know the behavior of the deer in depth. Our research method identifies individual deer using several steps where we initially take video feed which is further divided into several frames. The extracted frames are then cleaned and processed for the training efficiency. The cleaned frames are then sent to the Convolution Network where the Nested triplet loss is calculated for the maximum accuracy.