In this study, we report the curriculum of a programming course case study of senior citizens jointly implemented by the university and a local government in Japan. The objective of the course is to offer high-quality lifelong learning opportunities for retired seniors. The program also offers them necessary skills for impacting programming education in the local elementary schools, and the participatory action research (PAR) was adopted as a research method. Through a questionnaire and participant observation, we design the course by collecting the opinions of a lecturer or assistant to understand the manner in which the participants developed human relations and learning for one year. The research objectives are to study the learnability of the programming course and the course operation among differently aged participants. Through qualitative analysis, we observed distinct characteristics of senior learners with respect to their diversities in terms of motivation, background knowledge, and skills. The second course was taught by senior lecturers who had previously attended the course and the learnability of the second course was better than the previous one. With respect to the instructional design for senior citizens, scheduling, pacing, and diverse learning styles were observed to be the key. For future study, we attempt to address the conflicts among members and guarantee the quality of education for senior lecturers to support the teaching of programming in elementary schools. This study was supported by JSPS KAKENHI Grant Number JP18K02828.

In learning and development, students need to be made aware of their slips and mistakes in terms of acquiring the required knowledge, skills and competencies, especially, in active learning approaches. However, assessments may not necessarily lead to an effective understanding of student's errors. Most assessors are required to measure the extent of student's accurate output in terms of exam answers or practical assessments. Areas of failure tend to be overlooked and for this reason, learners at-risk of achieving poor results can become careless when completing assessments. In the present study, we examine the following research questions: (i) How can we simulate the landscape of data on both individual and team behaviour in terms of failure in their projects? (ii) How can we develop ways of identifying at-risk students in each team and support them immediately? Therefore, in order to address this problem, this research proposes an agent-based simulation of student projects, which considers both individual and team errors. This model is created on the basis of particular characteristics of individual learners within the team. We assume that individuals working within a team are subject to recognition-primed decision making when confronted with particular problems to solve. The adjustment proposed by this model includes analysing the problem using prior knowledge and planning as well as judgements on the suitability of particular solutions. This research will be further developed to identify at-risk learners in terms of investigating the areas they want to develop to achieve their learning goals in particular subjects and especially in the software development fields.

When a software failure is observed during testing or operation, developers traditionally execute the software program again for reproducing the failure to analyze the cause of the failure. However, failures are often hard to reproduce because they depend on factors that are hard to expressly control, such as concurrency and nondeterminism. This paper presents a novel experimental fault analysis process for such "hard-to-reproduce failures". The proposed process consists of three phases: assumption of a hypothesis for the cause of a failure, experiments to examine the hypothesis and confirmation of the experimental results. We formalized the process and implemented it by using model extraction and model checking. Model extraction acts as a bridge between the assumption and experiment. Experiments on failure reproduction are conducted using model checking. The results of the case studies show that the process and tools supporting the process enables developers to detect the cause of hard-to-reproduce failures in industrial software development.

Formal Methods has been recognized as a rigorous development methodology for hardware and software systems. In particular, model checking is well accepted as an effective verification method for hardware systems, safety/missioncritical systems and embedded systems. To foster this technology in industry, we recognize a need to develop educational materials to enhance learning the technology by students and practitioners. However, there are neither standard guidelines nor instructions how to teach this technology. In this paper, we will present the first draft of a body of knowledge on model checking called MCBOK to address this issue, and present lessons learned from its development experience.

Model checking is a powerful technique for verifying the correctness of a systempsilas specification. But even when the specification has been verified to be correct, there is still the question of whether the specification covers all the expected behaviors. One of the most important issues for verification is the sufficiency of verification items. In model checking, specification-level properties such as reachability are well-studied, but the sufficiency of a specification against the preceding requirements still remains a challenge.In this paper, we propose a model-checking process with goal oriented requirements analysis, in which goal descriptions in a natural language are systematically refined into linear temporal logic formulae. Furthermore, the coverage of the verification result can be evaluated against the goal model. We developed a tool that supports the process, and applied it to an example. This process lowers the technical barriers to model checking and improves the sufficiency of system verification.

As mobile computing becomes common, the battery issue of mobile computing devices has become increasingly notable. To this end, research and development of various power-conservation devices and methods are actively taking place. However, the conventional method of extending the battery life through power-conservation can never prevent the unintentional shutdowns of applications due to a dead battery. This research aims to realize the evacuation of applications on a mobile computing device to another device before the battery runs out by creating the application as a mobile agent. In particular, by introducing the concept of the Crisis Management Center, dynamic and smooth evacuation of multiple application agents will become possible. The paper explains and verifies the effectiveness of the EASTER (Escape Agent System from dying batTERy), a system developed for the purpose of recovering the applications when a battery is running out through the use of a mobile agent system.

This paper reports a directory server in a distributed middleware for realizing the interoperability between a wide variety of mobile agent systems. The ODP trader, an ITU-T recommendation for direction service, is customized for the specific requirements. The key ideas are (1) to extend the managed information so that program codes can be members, and (2) to provide Proxy Offer for utilizing services located outside the directory. Performance measurement shows that Proxy Offer is more efficient than dynamic property of the ODP trader in the current application.

We propose two new concepts, evolutional agent and field. The main purpose of the work is to provide a framework for building software which adapts to changes of requirements autonomously. In open networks, the adaptability to changes of requirements or environments is essential, while there are many free applications and components to serve various requirements. Focusing on this point, we introduce concurrent objects with meta-base architecture, agents, and fields, another kind of object. In our model, adaptive agents, called evolutional agents, adapt to changes by traversing a network and acquiring components as their own functions. Fields are receptacles of software components in networks. Agents evolve into enhanced ones by traveling to fields and acquiring components from the fields. Flage is a framework for building the software architecture based on these concepts.

We propose Flage, a language for building software modules (agents) which adapt to a change of environment in an open distributed system. Environments are defined as multiple agents and specifications which consist of constraints for cooperation among the agents. Flage provides a description of environments by the notion of agents and fields. We describe the concept of Flage and the adaptation technique.>