Presentation 2001/1/15
Deductive Refinement Verification Method based on Assume-Guarantee Style for Real-Time Software
Satoshi Yamane, Takashi Yamanokuchi,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) Real-time software has ongoing interactions with external environments, and consists of concurrent processes. It is important to verify whether real-time software is valid on not. In this paper, we propose a deductive refinement verfication method based on Pnueli's clocked transition modules. Especially, in order to avoid state explosion problems, our proposed method is realized by Assume-Guarantee Style, verifying receptiveness. Finally, we show our proposed method effective by some example.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) real-time software / Assume-Guarantee Style / deductive refinement verification / receptiveness
Paper # SS2000-31
Date of Issue

Conference Information
Committee SS
Conference Date 2001/1/15(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Software Science (SS)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Deductive Refinement Verification Method based on Assume-Guarantee Style for Real-Time Software
Sub Title (in English)
Keyword(1) real-time software
Keyword(2) Assume-Guarantee Style
Keyword(3) deductive refinement verification
Keyword(4) receptiveness
1st Author's Name Satoshi Yamane
1st Author's Affiliation Dept. of computer science, Kagoshima university()
2nd Author's Name Takashi Yamanokuchi
2nd Author's Affiliation Dept. of computer science, Kagoshima university
Date 2001/1/15
Paper # SS2000-31
Volume (vol) vol.100
Number (no) 569
Page pp.pp.-
#Pages 8
Date of Issue