DocumentCode
3251288
Title
Behavioral verification of distributed concurrent systems with BOBJ
Author
Goguen, Joseph ; Lin, Kai
Author_Institution
Dept. Comput. Sci. & Eng., California Univ., San Diego, CA, USA
fYear
2003
fDate
6-7 Nov. 2003
Firstpage
216
Lastpage
235
Abstract
Following a brief introduction to classical and behavioral algebraic specification, this paper discusses the verification of behavioral properties using BOBJ, especially its implementation of conditional circular coinductive rewriting with case analysis. This formal method is then applied to proving correctness of the alternating bit protocol, in one of its less trivial versions. We have tried to minimize mathematics in the exposition, in part by giving concrete illustrations using the BOBJ system.
Keywords
algebraic specification; formal verification; multiprocessing systems; protocols; rewriting systems; BOBJ; alternating bit protocol; behavioral algebraic specification; behavioral verification; conditional circular coinductive rewriting; correctness proving; distributed concurrent systems; Algebra; Computer science; Concrete; Concurrent computing; Hardware; Logic functions; Mathematics; Protocols; Software systems; Supercomputers;
fLanguage
English
Publisher
ieee
Conference_Titel
Quality Software, 2003. Proceedings. Third International Conference on
Print_ISBN
0-7695-2015-4
Type
conf
DOI
10.1109/QSIC.2003.1319106
Filename
1319106
Link To Document