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.

Automated Extraction of Secure Software from Proof Assistant Systems

Research Position

Various formal methods can be applied in order to achieve secure software systems, e.g.:

• Model Checking
• Formal Specification
• Theorem Proving

Among these, developers can apply so-called "proof assistant systems" to describe and determine whether certain operations of concern are secure. However, applying theorem proving on Hadoop MapReduce Applications is challenging for the following reasons:

• Definitions should be in functional style and built on the Calculus of Constructions. On the other hand, to execute functional program on Hadoop, Hadoop Streaming is required, which increases the required execution time significantly.
• Native Hadoop MapReduce applications should use the Iterator interfaces, which obviously introduce side effects.

Approach

• We propose a DSL whose semantics should be on the middle of definitions in functional style (for verification) and imperative style (for execution).
• We (step a) translate the DSL description into Coq descriptions which provide a formal syntax and semantics.
• Developer will (step 2) provide a proof to verify the DSL (step 1) on the basis of the given theorems which are used as the specifications.
• In the last step, we (step b) automatically generate Scala code, which can be compiled to Java bytecode.

Recently, we are focusing on the following problems in particular:

• It is critically important tIt is important to ensure that there is no gap regarding the semantics between the DSL description and the Scala program. This should be done in a formal way.
• Our approach raises a challenge: we need a proof techniques that supports state transactions which is far beyond the possibilities of what Coq supports. There is a need to propose a new support for theorem proving.

Deriving Event-B Specifications from Requirements through Analysis of Vocabulary

Nowadays, methods to define the specification of a software in formal languages are attracting wide attentions since they improve the quality and reliability of deliverables. On the other hand, specifications in natural languages are still essential, as they are suitable for understanding and communication. Therefore, developers who use formal specification methods have to construct a formal specification from the natural language one. This process is difficult and requires deep knowledge about the method. Our goal is to reduce this kind of difficulty.

Our current target is Event-B, a formal specification method that has been actively investigated in recent years. The notable feature of this method is the support of stepwise refinement. Stepwise refinement enables developers to start by specifying an abstract (but strict) specification and to gradually introduce complex aspects with proof. Thus, the method reduces the complexity of specifications in a rigid way. However, making use of the stepwise refinement in a consistent way is a difficult process. Especially, refinement planning, i.e. deciding which elements in the natural language specification are included in each refinement step requires extensive knowledge and experience. We aim to mitigate this difficulty.

Our proposed method includes the definition of typical refinement patterns, e.g. the "concrete specification that includes a controller, its peripherals, and their relation" refines an "abstract specification, which specifies only the controller". The method includes a step to tag "keys" of patterns (e.g. controller, peripheral, etc. in the above example) and components of the target system. In the next step, the plan is determined through dependency/permission analysis of the tagged components. Finally, a natural language specification is restructured according to the plan and translated into an Event-B specification. By applying this method, the process obtaining an Event-B specification becomes easier. Moreover, it helps getting the traceability between a natural language specification and the formal one.

Emulating Non-blocking IO on Top of Blocking IO in Java PathFinder

Java PathFinder (JPF) is a model checker developed by NASA that can perform model checking on Java applications. It is impossible to do model checking with JPF on applications that have side effects (such as IO operations). However, we intend to extend JPF in a way that it can be applied to such applications.

In this research, our goal is to support non-blocking IO, which is not supported by JPF. In other work, a blocking IO is already supported and in order to support a non-blocking IO, either 1) non-blocking IO operations are emulated on top of a blocking IO or 2) a non-blocking IO have to be implemented from scratch. However, implementing these operations from scratch is time consuming. Moreover, it will produce a lot of duplicated code and as a consequence raise the maintenance costs. Therefore, we emulate a non-blocking IO on top of a blocking IO.

To emulate a non-blocking IO in a model checker, all state transitions have to be covered. The key idea is that a non-blocking IO can be emulated by a blocking IO and logical flags. We use a blocking IO underneath and control logical availability flags. For example, a non-blocking SocketChannel has the following state transitions.

Please note that the SocketChannel transits to the Pending or Connected state from the Opened state in a non-deterministic way. To emulate this behavior, we physically connect first and set the pending flag non-deterministically by using JPF’s choice generator. If the flag is true we transit to the Pending state and if not we transit to the Connected state.

In the same way, we emulate the other non-deterministic transitions and emulate a non-blocking IO on top of a blocking IO.

Like above we support a non-blocking IO, making possible to model check applications with a non-blocking IO (which can be model checked by the original JPF) in JPF.

Members

• Yoshinori Tanabe (Specially Appointed Professor)
• Fan Jiang (D3)
• Shouichi Kamiya (M2)
• Tsutomu Kobayashi (M2)

Contact Information

Tsutomu Kobayashi :

Research Results

Selected Publications