Automatic abstraction for model checking software systems with interrelated numeric constraints

Research output: Contribution to conferencePaper

11 Scopus citations

Abstract

Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and nonlinear constraints over the input variables. Various model abstraction techniques have been proposed to address this problem. In this paper, we wish to propose domain abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Oar technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system. Our technique is automatable with some minor restrictions.

Original languageEnglish (US)
Pages164-174
Number of pages11
StatePublished - Dec 1 2001
Event8th Eiropean Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9) - Vienna, Austria
Duration: Sep 10 2001Sep 14 2001

Other

Other8th Eiropean Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9)
CountryAustria
CityVienna
Period9/10/019/14/01

Keywords

  • Domain abstraction
  • Model checking software systems
  • Numeric constraints

Fingerprint Dive into the research topics of 'Automatic abstraction for model checking software systems with interrelated numeric constraints'. Together they form a unique fingerprint.

  • Cite this

    Choi, Y., Rayadurgam, S., & Heimdahl, M. P. E. (2001). Automatic abstraction for model checking software systems with interrelated numeric constraints. 164-174. Paper presented at 8th Eiropean Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), Vienna, Austria.