CONFERENCIANTE: Kokichi Futatsugi (JAIST, Japón)

TITULO: Generic Proof Scores for Generate & Check Method in CafeOBJ

FECHA: Lunes 9/3/2015 a las 12:00

LUGAR: Salón de grados B - ETSI Informática

RESUMEN

Constructing specifications and verifying them in the upstream of system/software development are still one of the most important challenges in system/software development and engineering. Proof scores are intended to meet this challenge. A system and the system's properties are specified in an executable algebraic specification language (CafeOBJ in our case).  Proof scores are described also in the same specification language for checking whether the system specifications imply the property specifications. The generate & check method is a theorem proving method for transition systems based on (1) generation of finite state patters that cover all possible infinite states, and (2) checking the validities of verification conditions for each of the finite state patterns. I this talk, generic proof scores for the generate & check method in CafeOBJ are described.  The generic proof scores codify the generate & check method as parameterized modules in the CafeOBJ language independently of specific systems to which the method applies.  Proof scores for a specific system can be obtained by substituting the parameter modules of the parameterized modules with the specification modules of the specific system. The effectiveness of the generic proof scores is demonstrated by applying them to simple but non-trivial examples.

SHORT BIO:

Kokichi Futatsugi is a professor at Graduate School of Information Science, JAIST (Japan Advanced Institute of Science and Technology). 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. CafeOBJ adopts hidden algebra and rewriting logic as its underlying logics and its application areas include design and validation of fundamental and important systems such as component based systems, security/safety systems, computer language systems, etc.  Some parts of research around CafeOBJ are being conducted in cooperation with IPA (Information-Technology Promotion Agency, Tokyo, Japan), SRI (California, USA), Univ. of California at San Diego (USA), Univ. of Munich (Germany), ETL (Electrotechnical Lab.,Tsukuba, Japan), and several other companies and universities in Japan.