Presentation	2006-06-22 Some Cases on Model-Checking of Finite-state Automaton with Constraints Shin NAKAJIMA,
PDF Download Page	PDF download Page Link
Abstract(in Japanese)	(See Japanese page)
Abstract(in English)	Although the model-checking method is a powerful tool for system verification, the target system should be represented with a finite-state space, which is the very limitation of the method. This paper proposes "constraint automaton", which is an extended finite-state automaton with a notion of data constraints. The automaton keeps track of the constraints along its execution, state-transitions, and performs the satisfiability checking and constraint solving as needed. The paper also discusses how the constraint automaton is represented in Maude, which makes it possible to perform the model-checking of LTL formula against the constraint automaton by using the Maude/LTL library.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	Model Checking / Algebraic Specification / Constraint System / Maude / Symbolic Execution
Paper #	SS2006-16
Date of Issue

Conference Information
Committee	SS
Conference Date	2006/6/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)	Some Cases on Model-Checking of Finite-state Automaton with Constraints
Sub Title (in English)
Keyword(1)	Model Checking
Keyword(2)	Algebraic Specification
Keyword(3)	Constraint System
Keyword(4)	Maude
Keyword(5)	Symbolic Execution
1st Author's Name	Shin NAKAJIMA
1st Author's Affiliation	National Institute of Informatics:SORST-JST()
Date	2006-06-22
Paper #	SS2006-16
Volume (vol)	vol.106
Number (no)	120
Page	pp.pp.-
#Pages	6
Date of Issue