Improving the precision of INCA by eliminating solutions with spurious cycles

Author

Siegel, Stephen F. ; Avrunin, George S.

Author_Institution

Dept. of Comput. Sci., Massachusetts Univ., Amherst, MA, USA

Volume

28

Issue

2

fYear

2002

fDate

2/1/2002 12:00:00 AM

Firstpage

115

Lastpage

128

Abstract

The Inequality Necessary Condition Analyzer (INCA) is a finite-state verification tool that has been able to check properties of some very large concurrent systems. INCA checks a property of a concurrent system by generating a system of inequalities that must have integer solutions if the property can be violated. There may, however, be integer solutions to the inequalities that do not correspond to an execution violating the property. INCA thus accepts the possibility of an inconclusive result in exchange for greater tractability. We describe here a method for eliminating one of the two main sources of these inconclusive results

Keywords

concurrency theory; finite state machines; formal verification; software tools; INCA; Inequality Necessary Condition Analyzer; finite-state verification tool; inequalities; integer solutions; spurious cycle solution elimination; very large concurrent systems; Automata; Computer Society; Costs; Explosions; Linear programming; State-space methods; System recovery; System testing;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.988494

Filename

988494