TY - GEN
T1 - Towards automatic determination of problem bounds for object instantiation in static model verification
AU - Soeken, Mathias
AU - Wille, Robert
AU - Drechsler, Rolf
PY - 2011
Y1 - 2011
N2 - The application of formal methods in the detection of incon- sistencies and design aws within models has been intensely studied in recent years. Since consistency checking is in prin- ciple undecidable due to the infinite number of possible sys- tem states, problem bounds have to be defined making the analysis tractable. However, defining these problem bounds requires detailed design knowledge and, thus, impedes an automatic verification ow. In this paper, we present first ideas and results of how to automatically determine valid problem bounds for con- sistency checking algorithms. For this purpose, we make use of automatic proof engines for linear integer arithmetic. We describe the approach by means of class diagrams given in the Unified Modeling Language (UML) extended by con- straints given in the Object Constraint Language (OCL).
AB - The application of formal methods in the detection of incon- sistencies and design aws within models has been intensely studied in recent years. Since consistency checking is in prin- ciple undecidable due to the infinite number of possible sys- tem states, problem bounds have to be defined making the analysis tractable. However, defining these problem bounds requires detailed design knowledge and, thus, impedes an automatic verification ow. In this paper, we present first ideas and results of how to automatically determine valid problem bounds for con- sistency checking algorithms. For this purpose, we make use of automatic proof engines for linear integer arithmetic. We describe the approach by means of class diagrams given in the Unified Modeling Language (UML) extended by con- straints given in the Object Constraint Language (OCL).
UR - http://www.scopus.com/inward/record.url?scp=84856895588&partnerID=8YFLogxK
U2 - 10.1145/2095654.2095657
DO - 10.1145/2095654.2095657
M3 - Conference contribution
AN - SCOPUS:84856895588
SN - 9781450309141
T3 - ACM International Conference Proceeding Series
BT - Proc. of the 8th Int. Workshop, MoDeVVa 2011
T2 - 8th International Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa 2011 - Co-located with the 14th International Conference on Model Driven Engineering Languages and Systems, MoDELS
Y2 - 17 October 2011 through 17 October 2011
ER -