Formal treatment of a family of fixed-point problems on graphs by CafeOBJ

Author

Tamai, Tetsuo

Author_Institution

Interfaculty Initiative in Inf. Studies, Tokyo Univ., Japan

fYear

2000

fDate

2000

Firstpage

67

Lastpage

74

Abstract

A family of well-known problems on graphs, including the shortest path problem and the data flow analysis problem, can be uniformly formulated as a fixed-point problem on graphs. We specify this problem and its solution algorithm in a highly abstract manner, fully exploiting the parametrized module construct of CafeOBJ, an algebraic specification language. The objective of our research is to explore the effectiveness of formal methods, applying them not just to specific safety-critical programs but to general problems covering a wide range of applications

Keywords

algebraic specification; data flow analysis; fixed point arithmetic; graph theory; mathematics computing; minimisation; object-oriented languages; object-oriented methods; safety-critical software; specification languages; CafeOBJ; abstract problem specification; algebraic specification language; data flow analysis problem; fixed-point problems; formal methods; graphs; safety-critical programs; shortest path problem; Algebra; Application software; Data analysis; Hardware; Information analysis; Logic; Protocols; Shortest path problem; Software safety; Specification languages;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Engineering Methods, 2000. ICFEM 2000. Third IEEE International Conference on

Conference_Location

York

Print_ISBN

0-7695-0822-7

Type

conf

DOI

10.1109/ICFEM.2000.873806

Filename

873806