Toward Automation for Model Checking Requirement Specifications with Numeric Constraints

Loading...
Thumbnail Image

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Toward Automation for Model Checking Requirement Specifications with Numeric Constraints

Published Date

2002

Publisher

Type

Report

Abstract

Model checking techniques have not been effective in important classes of software systems---systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the system variables. Various model abstraction techniques have been proposed to address this problem, but their effectiveness in practice is limited by two factors; first, the abstraction process is manual and requires a great deal of ingenuity, and, second, the abstraction may be coarse and introduce too many spurious behaviors to provide meaningful analysis results. In this paper, we wish to propose domain reduction abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition systems. Our technique is automatable with some minor restrictions. We provide formal proofs for the theoretical soundness of the technique, algorithms for automation, and an illustration of the approach with examples.

Keywords

Description

Associated research group: Critical Systems Research Group

Related to

Replaces

License

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Requirements Engineering Journal, Vol-7, Issue 4, pp. 225-242 (2002)

Suggested citation

Choi, Yunja; Rayadurgam, Sanjai; Heimdahl, Mats. (2002). Toward Automation for Model Checking Requirement Specifications with Numeric Constraints. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217340.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.