Formal Methods (MALACS)

Overview

The MALACS (Models And Languages for Correct Software) group studies formal methods related to software development, including methods for specification, verification and code generation.

Formal methods involve the use of precise mathematical models, languages, and tools to automate various software development tasks such as design, testing, verification, synthesis, etc. Model checking in particular has been an extremely successful area in the last few decades, with the ACM Turing award of 2007 being shared by Edmund M Clarke, E Allen Emerson and Joseph Sifakis, for their roles in its development. It is essential for the development of various kinds of critical software systems, including industrial, healthcare, and aerospace systems.

Research Topics

Network model checking with Java PathFinder

Java PathFinder (JPF) is a software model checker being developed as open-source software by many people, especially by developers working at NASA. We are developing techniques for JPF to model-check networked applications, that is, programs communicating each other.

JPF, as well as many other software model checkers, verifies only one process at a time. Usually, there are many processes that communicate with each other. Therefore, if only one process is regarded as the target of model checking, the process communication might fail because one process may backtrack while the others do not expect that. As a solution to the problem, we have proposed an "I/O cache layer", which observes and synchronizes the communication between the target process and the other processes. We have implemented this layer and it is now being distributed with JPF.

We plan to utilize this technology as a basis to verify the infrastructure of a cloud computing environment. This work has been done as a collaborative research with Cyrille Artho, Masami Hagiya, Eric Platon and Mitsuharu Yamamoto.

Multi-valued Semantics of Modal Mu-calculi

As applications of formal methods, techniques to directly verify the source code have been widely developed. One of the key methods is abstraction. The size of the set of execution states of a program is generally too huge to allow an analysis of the state space directly. Abstraction methods tie a certain number of similar concrete states into an abstract state in order to enable this analysis. We have proposed a method that offers this abstraction for pointer-manipulating programs, i.e. programs that handle data structures constructed from pointers, such as lists, trees, or DAGs. This method utilizes a group of modal logics called enriched modal mu-calculi.

Our current interest includes N-infinity-valued Kripke structures for verification of termination. N-infinity is the set of natural numbers plus the maximum element infinity. By introducing an appropriate algebraic structure, we can consider the elements of N-infinity as "truth-values" of the formulae. Complete truth and falsehood are 0 and infinity, respectively; and the others are intermediate values. It can be shown that we reduced the termination problem of various pointer-manipulating programs into the satisfiability problem of an N-infinity-valued Kripke structure. We aim at revealing decision procedures of the problem, and as a prerequisite, model-checking procedures of the structure.

In these years the Japanese industry has very strong interest in use of formal specifications. On the other hand there are strong concerns on cost or difficulty in construction rigorous and complete specifications. There are also indifference by agile or quality-assurance communities, given a typical impression of methods that work intensively on specification models.

This work aims at providing a tool that leverages techniques of formal specifications partially or gradually, from skeletons before construction of program behavior. The input to the tool includes descriptions of specifications (contracts) or test strategies, in addition to Java skeletons. It is notable that these descriptions can be fragmented, such as case conditions or examples, even empty (only skeletons). The tool uses constraint solvers and search and present expected test cases for the descriptions.

This tool can be used to enhance the current human tasks by presenting examples, which are checked manually. It can be also used to gradually construct complete formal specifications, by repeatedly adding descriptions through examination of examples. Thus the tool aims at the minimum usages of formalization and automation. It also provides a common means for test-driven development, formal specifications and test design.

Systematic Abstraction Level Controlling in Stepwise Refinement of Formal Specifications

Systematic analysis of software in early phases of development is important. Formal specification methods are effective for the purpose. Especially, formal specification by using stepwise refinement enables developers to deal with complexity of software and analyze in a rigorous way. Nowadays this approach attracts developers' attention. For example, Event-B receives wide attention since it is aimed at stepwise refinement support.

Usually informal documents are created before creation of formal specification. In development using methods such as Event-B, developers should plan what elements in informal documents are reflected to each specification. In this planning, the plan must obey rules of formal specification method. On the other hand, the plan should be understandable for developers. However, fulfilling both of them is difficult. For example, excessive distribution of introducing elements in the system often causes violation of the rules. On the other hand, developers are so careful about obeying rules that they often make models difficult to understand. Thus planning good refinements needs many trial-and-errors.

There are many things developers have to decide during planning. We classify them into two groups, namely things that must be judged by developers and things that can be automatically judged from rules of the formal specification method. We propose a method to do trial-and-error automatically by getting information about the latter. Specifically, we proposed several goals that developers should fulfill during refinement and proposed a method to search plan considering priorities of the goals. We are conducting experiments using toy examples of Event-B.

Members

  • Yoshinori Tanabe (Specially Appointed Professor)
  • Fuyuki Ishikawa (Associate Professor)
  • Tsutomu Kobayashi (D1)
  • Fernando Tarin (D1)

Contact Information

Tsutomu Kobayashi:

Research Results

Selected Publications

  1. Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden, Systematic Planning of Refinement in Event-B, The 4th Rodin User and Developer Workshop at iFM 2013, June 2013 (to appear)
  2. Tsutomu Kobayashi and Shinichi Honiden: Towards Refinement Strategy Planning for Event-B, Workshop on the experience of and advances in developing dependable systems in Event-B (DS-Event-B'12) in conjunction with ICFEM, November 2012
  3. Fuyuki Ishikawa, Toward Customizable and Bi-directionally Traceable Transformation between VDM++ and Java, The 9th Overture/VDM Workshop at FM 2011, June 2011
  4. Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya: Modal μ-calculus on min-plus algebra N-infinity, Computer Software (Accepted)
  5. Alexis Goyet, Masami Hagiya and Yoshinori Tanabe: Decidability and undecidability results on the modal mu-calculus with a natural number-valued semantics, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Lecture Notes in Artificial Intelligence, Vol.6188, 2010, pp.148-160.
  6. Yoshinori Tanabe and Masami Hagiya: Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus. 6th Workshop on Fixed Points in Computer Science (FICS 2009), Coimbra, Portugal, 12-13 September 2009, pp. 108--115.
  7. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto: Cache-Based Model Checking of Networked Applications: From Linear to Branching Time. ASE 2009: 447-458
  8. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe: Efficient Model Checking of Networked Applications. TOOLS (46) 2008: 22-40