Recent Developments on Specification and Verification with CafeOBJ
Japan Advanced Institute of Science and Technology
Japan
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
Constructing specifications and verifying them in the upstream of software development are still one of the most important challenges in formal software engineering. It is because quite a few critical bugs are caused at the level of domains, requirements, and/or designs specifications. Proof scores are intended to meet this challenge. In the proof score approach, an executable algebraic specification language (i.e. CafeOBJ in our case) is used to specify a system and system properties, and the reduction (or rewriting) engine of the language is used as a proof engine to prove that the system satisfy the properties of interest.
Proof plans for verifying the system properties are coded into proof scores, and are also written in the algebraic specification language. Usually, a proof score describes modules and predicates in the modules that constitute a sufficient condition for verifying a system property. The language processor interprets the specification and proof score and verifies the validity of the sufficient condition by checking all the predicates with reductions. Logical soundness of the reductions is guaranteed by the fact that the reductions are consistent with the equational reasoning with the equations in the specification and the proof score. Effective coordination of inference (a` la theorem proving) and search (a` la model checking) is important for making proof scores more effective and powerful, and we have developed several techniques.
In this talk, recent developments around CafeOBJ proof score method for verifying specifications are surveyed. Several developed proof score styles as open-close, spec-calculus, gen&check are explained, and their relationships and future potential is discussed.
Biodata:
Kokichi Futatsugi is a Research Professor of JAIST (Japan Advanced Institute of Science and Technology). Before getting a full professorship at JAIST in 1993, he was working for ETL (Electrotechnical Lab.) of Japanese Government and was assigned to be a Chief Senior Researcher of ETL in 1992. He stayed at SRI (Stanford Research Institute) in California as an International Fellow for one year from 1983 to 1984. His primary research goal is to design and develop new computer languages which can open up new application areas, and/or improve the current software technology. His current approach for this goal is CafeOBJ formal specification language.
CafeOBJ is multi-paradigm formal specification language which is a modern successor of the most noted algebraic specification language OBJ. The OBJ language has been designed and developed by K.Futatsugi, J.Goguen, J.-P.Jouannaud, and J.Meseguer at SRI in 1984.
Some of researches and developments around CafeOBJ is being conducted in cooperation with IPA (Information-Technology Promotion Agency, Tokyo, Japan), SRI (California, USA), Univ. of California at San Diego (USA), and Univ. of Munich (Germany), ETL (Electrotechnical Lab.,Tsukuba, Japan), and several companies and universities in Japan.
Kokichi Futatsugi got the fellow award of Japan Society of Software Science and Technology in 2008 and got the distinguished research award of ETL in 1991.
Kokichi Futatsugi was an associate editor of TOSEM (ACM Transactions of Software Engineering and Methodology) from 1995 to 2002. He also worked for many international conferences, symposiums, workshops as General Chair and PC chair, i.e., General Chair of 14th International Conference on Formal Engineering Methods (ICFEM'12), Nov 2012, Kyoto,Japan and PC Co-Chair of 20th International Conference on Software Engineering (ICSE'98), April 1998, Kyoto, Japan.