Bounded Verification of Software Models: Challenges and Opportunities
Abstract
Ensuring the absence of bugs in a software system is an important but very challenging problem. Early error detection within the development process reduces the cost of finding and fixing defects. Thus, the analysis of software models can improve its final quality and reduce its development costs.
A promising research direction in this field is the use of boolean satisfiability (SAT) or constraint programming (CP) solvers to perform bounded verification. Bounded verification consists in formally checking the absence of errors within a finite space defined as a parameter of the analysis. This type of analysis is usually fast in practice and provides informative feedback. However, it is computationally complex in general and lacks conclusive results outside the verification bounds provided as parameters.
In this paper, we discuss recent trends and results in the application of bounded verification to a specific field within software engineering: the analysis of models of a software system. Furthermore, we will discuss promising contributions that can build upon previous work to improve its applicability in practice within the software industry.
A promising research direction in this field is the use of boolean satisfiability (SAT) or constraint programming (CP) solvers to perform bounded verification. Bounded verification consists in formally checking the absence of errors within a finite space defined as a parameter of the analysis. This type of analysis is usually fast in practice and provides informative feedback. However, it is computationally complex in general and lacks conclusive results outside the verification bounds provided as parameters.
In this paper, we discuss recent trends and results in the application of bounded verification to a specific field within software engineering: the analysis of models of a software system. Furthermore, we will discuss promising contributions that can build upon previous work to improve its applicability in practice within the software industry.
Keywords
Software Engineering; Software Quality; Formal Methods; Formal Verification; Model-Driven Engineering (MDE); Constraint Programming; Boolean Satisfiability (SAT); UML; OCL; Model Transformations
Full Text:
PDF
The texts published in this publication are – unless otherwise indicated – covered by the Creative Commons Attribution-Non commercial-No derivative works 3.0 Spain licence. They may be copied, distributed and broadcast provided that the author, the publication and the institutions that publish them (IN3 Working Paper Series, IN3 and UOC) are cited. Commercial use and derivative works are not permitted. The full licence can be consulted on http://creativecommons.org/licenses/by-nc-nd/3.0/deed.en.