A concurrent system consists of multiple processes that are run simultaneously. The execution orders of these processes are defined by a scheduler. In model checking techniques, the scheduling policy is closely related to the search algorithm that explores all of the system states. To ensure the correctness of the system, the scheduling policy needs to be taken into account during the verification. Current approaches, which use fixed strategies, are only capable of limited kinds of policies and are difficult to extend to handle the variations of the schedulers. To address these problems, we propose a method using a domain-specific language (DSL) for the succinct specification of different scheduling policies. Necessary artifacts are automatically generated from the specification to analyze the behaviors of the system. We also propose a search algorithm for exploring the state space. Based on this method, we develop a tool to verify the system with the scheduler. Our experiments show that we could serve the variations of the schedulers easily and verify the systems accurately.

Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. The existing works focus on verifications where the specifications are described using temporal logics or using the same languages as that used to describe the designs. Our work considers cases where the specifications and the designs are described using different languages. To verify such cases, we propose a framework to check if a design conforms to its specification based on their simulation relation. Specifically, we define the semantics of the specifications and the designs commonly as labelled transition systems (LTSs). We appreciate LTSs since they could interpret information about the system and actions that the system may perform as well as the effect of these actions. Then, we check whether a design conforms to its specification based on the simulation relation of their LTS. In this paper, we present our framework for the verification of reactive systems, and we present the case where the specifications and the designs are described in Event-B and Promela/Spin, respectively. We also present two case studies with the results of several experiments to illustrate the applicability of our framework on practical systems.

We demonstrated that load balancing using actual subscriber extension numbers was practical and effective against traffic congestion after a disaster based on actual data. We investigated the ratios of the same subscriber extension numbers in each prefecture and found that most of them were located almost evenly all over the country without being concentrated in a particular area. The ratio of every number except for the fourth-last digit in the last group of four numbers in a telephone number was used almost equally and located almost evenly all over the country. Tolerance against overload in the last, second-, and third-last single digits stays close to that in the ideal situation if we assume that each session initiation protocol server has a capacity in accordance with the ratio of each number on every single digit in the last group of four numbers in Japan. Although tolerance against overload in double-, triple-, and quadruple-digit numbers does not stay close to that in the ideal situation, it still remains sufficiently high in the case of double- and triple-digit numbers. Although tolerance against overload in the quadruple-digit numbers becomes low, disaster congestion is still not likely to occur in almost half of the area of Japan (23 out of 47 prefectures).

Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al.'s framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled.

In multiprocessors, memory models are introduced to describe the executions of programs among processors. Relaxed memory models, which relax the order of executions, are used in the most of the modern processors, such as ARM and POWER. Due to a relaxed memory model could change the program semantics, the executions of the programs might not be the same as our expectation that should preserve the program correctness. In addition to relaxed memory models, the way to execute an instruction is described by an instruction semantics, which varies among processor architectures. Dealing with instruction semantics among a variety of assembly programs is a challenge for program verification. Thus, this paper proposes a way to verify a variety of assembly programs that are executed under a relaxed memory model. The variety of assembly programs can be abstracted as the way to execute the programs by introducing an operation structure. Besides, there are existing frameworks for modeling relaxed memory models, which can realize program executions to be verified with a program property. Our work adopts an SMT solver to automatically reveal the program executions under a memory model and verify whether the executions violate the program property or not. If there is any execution from the solver, the program correctness is not preserved under the relaxed memory model. To verify programs, an experimental tool was developed to encode the given programs for a memory model into a first-order formula that violates the program correctness. The tool adopts a modeling framework to encode the programs into a formula for the SMT solver. The solver then automatically finds a valuation that satisfies the formula. In our experiments, two encoding methods were implemented based on two modeling frameworks. The valuations resulted by the solver can be considered as the bugs occurring in the original programs.

The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming languages. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. A TRS cannot, however, directly handle higher-order functions that are widely used in functional programming languages. In this paper, we propose a higher-order KB procedure that extends the KB procedure to the framework of a simply-typed term rewriting system (STRS) as an extended TRS that can handle higher-order functions. We discuss the application of this higher-order KB procedure to a certification technique called inductionless induction used in program verification, and its application to fusion transformation, a typical kind of program transformation.

OSEK/VDX, a standard for an automobile OS, has been widely adopted by many manufacturers to design and develop a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more complex applications are be developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. To ensure the reliability of developed applications, model checking as an exhaustive technique can be applied to discover subtle errors in the development process. Many model checkers have been successfully applied to verify sequential software and general multi-threaded software. However, it is hard to directly use existing model checkers to precisely verify OSEK/VDX applications, since the execution characteristics of OSEK/VDX applications are different from the sequential software and general multi-threaded software. In this paper, we describe and develop an approach to translate OSEK/VDX applications into sequential programs in order to employ existing model checkers to precisely verify OSEK/VDX applications. The value of our approach is that it can be considered as a front-end translator for enabling existing model checkers to verify OSEK/VDX applications.