Presentation	2000/1/18 Fomal specification and deductive verification based on Timed Statechart Satoshi Yamane,
PDF Download Page	PDF download Page Link
Abstract(in Japanese)	(See Japanese page)
Abstract(in English)	Hard real-time systems have ongoing interactions with external environments, and consist of concurrent processes. It is important to verify whether hard real-time systems satisfy safety and liveness properties or not. In this paper, we integrally specify concurrency and timing constraints, functions using our proposed timed statechart. Moreover, we represent operational semantics of timedstatechart using Pnueli's clocked transition systems. Next we can verify whether timed statechart satisfy safety and liveness properties or not by deductive proofs. Finally, we propose a refinement verification rule and verify whether concretespecification refines abstract specification or not.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	timed statechart / deductive verification / temporal logic / refinement
Paper #	SS99-54
Date of Issue

Conference Information
Committee	SS
Conference Date	2000/1/18(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)	Fomal specification and deductive verification based on Timed Statechart
Sub Title (in English)
Keyword(1)	timed statechart
Keyword(2)	deductive verification
Keyword(3)	temporal logic
Keyword(4)	refinement
1st Author's Name	Satoshi Yamane
1st Author's Affiliation	Dept. of computer science, Kagoshima university()
Date	2000/1/18
Paper #	SS99-54
Volume (vol)	vol.99
Number (no)	547
Page	pp.pp.-
#Pages	8
Date of Issue