Smart Bound Selection for the Verification of UML/OCL Class Diagrams

Clarisó, Robert; GONZALEZ PEREZ, Carlos Alberto; CABOT, Jordi

doi:10.1109/TSE.2017.2777830

Request a copy

Article (Scientific journals)

Smart Bound Selection for the Verification of UML/OCL Class Diagrams

Clarisó, Robert; GONZALEZ PEREZ, Carlos Alberto; CABOT, Jordi

2019 • In IEEE Transactions on Software Engineering

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/10993/33832

DOI
10.1109/TSE.2017.2777830

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

TSE2777830.pdf

Author preprint (849.33 kB)

Request a copy

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Formal Verification; Constraint Propagation; Class Diagram

Abstract :

[en] Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded verification techniques, e.g., SAT or constraint programming (CP) solvers. Bounded verification detects faults efficiently but, on the other hand, the absence of faults does not guarantee a correct behavior outside the bounded domain. Hence, choosing suitable bounds is a non-trivial process as there is a trade-off between the verification time (faster for smaller domains) and the confidence in the result (better for larger domains). Unfortunately, bounded verification tools provide little support in the bound selection process. In this paper, we present a technique that can be used to (i) automatically infer verification bounds whenever possible, (ii) tighten a set of bounds proposed by the user and (iii) guide the user in the bound selection process. This approach may increase the usability of UML/OCL bounded verification tools and improve the efficiency of the verification process.

Disciplines :

Computer science

Author, co-author :

Clarisó, Robert; Universitat Oberta de Catalunya > IT, Multimedia and Telecommunication Department

GONZALEZ PEREZ, Carlos Alberto ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)

CABOT, Jordi ; ICREA

External co-authors :

yes

Language :

English

Title :

Smart Bound Selection for the Verification of UML/OCL Class Diagrams

Publication date :

2019

Journal title :

IEEE Transactions on Software Engineering

ISSN :

0098-5589

eISSN :

1939-3520

Publisher :

Institute of Electrical and Electronics Engineers, New York, United States - New York

Peer reviewed :

Peer Reviewed verified by ORBi

Focus Area :

Security, Reliability and Trust

Additional URL :

https://doi.org/10.1109/TSE.2017.2777830

Available on ORBilu :

since 03 January 2018

Statistics

Number of views

232 (34 by Unilu)

Number of downloads

3 (3 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

WoS citations^™

Bibliography

M. Petre, "UML in practice," in Proc. Int. Conf. Softw. Eng., 2013, pp. 722-731.
E. Torlak, M. Taghdiri, G. Dennis, and J. Near, "Applications and extensions of Alloy: Past, present, and future," Math. Struct. Comput. Sci., vol. 23, pp. 915-933, 2013.
J. Whittle, J. Hutchinson, and M. Rouncefield, "The state of practice in Model-Driven engineering," IEEE Softw., vol. 31, no. 3, pp. 79-85, May/Jun. 2014.
D. Berardi, D. Calvanese, and G. D. Giacomo, "Reasoning on UML class diagrams," Artif. Intell., vol. 168, no. 1-2, pp. 70-118, 2005.
C. A. Gonzalez and J. Cabot, "Formal verification of static software models in MDE: A systematic review," Inf. Softw. Tech., vol. 56, no. 8, pp. 821-838, 2014.
M. Cadoli,D. Calvanese,G.D.Giacomo, and T. Mancini, "Finite satisfiability of UML class diagrams by constraint programming," in Proc. Workshop CSP Tech. Immediate Appl. (CSPIA 2004), 2004, pp. 2-16.
S. Ali, M. Z. Iqbal, A. Arcuri, and L. C. Briand, "Generating test data from OCL constraints with search techniques," IEEE Trans. Softw. Eng., vol. 39, no. 10, pp. 1376-1402, Oct. 2013.
A. D. Brucker and B. Wolff, "The HOL-OCL book," ETH Zurich, Zurich, Switzerland, Tech. Rep. 525, 2006.
J. Cabot, R. Clariso, and D. Riera, "On the verification of UML/ OCL class diagrams using constraint programming," J. Syst. Softw., vol. 93, pp. 1-23, 2014.
K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, "On challenges of model transformation from UML to Alloy," Softw. Syst. Model., vol. 9, no. 1, pp. 69-86, 2010.
M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla, and R. Drechsler, "Verifying UML/OCL models using boolean satisfiability," in Proc. Design Autom. Test Eur. Conf. Exhib., 2010, pp. 1341-1344.
C. A. Gonzalez, F. Buttner, R. Clariso, and J. Cabot, "EMFtoCSP: A tool for the lightweight verification of EMF models," in Proc. 1st Int. Workshop Formal Methods Softw. Eng.: Rigorous Agile Approaches, 2012, pp. 44-50.
M. Kuhlmann and M. Gogolla, "From UML and OCL to relational logic and back," in Proc. Int. Conf. Model Driven Eng. Languages Syst., 2012, pp. 415-431.
S. Maoz, J. O. Ringert, and B. Rumpe, "CD2Alloy: Class diagrams analysis using Alloy revisited," in Proc. Int. Conf. Model Driven Eng. Languages Syst., 2011, pp. 592-607.
L. Bordeaux, G. Katsirelos, N. Narodytska, and M. Y. Vardi, "The complexity of integer bound propagation," J. Artif. Intell. Res., vol. 40, pp. 657-676, 2011.
D. Marinov, "Automatic testing of software with structurally complex inputs," PhD Thesis, Department of Electrical Engineering anc Computer Science, Massachussets Institute of Technology Cambridge, MA, USA, 2005, http://hdl.handle.net/1721.1/30161
J. Oetsch, M. Prischink, J. Puhrer, M. Schwengerer, and H. Tompits, "On the small-scope hypothesis for testing answer-set programs," in Proc. 13th Int. Conf. Principles Know. Representation Reasoning, 2012, pp. 43-53.
F. Yu, T. Bultan, and E. Peterson, "Automated size analysis for OCL," in Proc. 6th Joint Meeting Eur. Softw. Eng. Conf. ACM SIGSOFT Symp. Foundations Softw. Eng., 2007, pp. 331-340.
R. Clariso, C. A. Gonzalez, and J. Cabot, "Towards domain refinement for UML/OCL bounded verification," in Proc. Softw. Eng. Formal Methods, 2015, pp. 108-114.
A. Queralt and E. Teniente, "Verification and validation of UML conceptual schemas with OCL constraints," ACM Trans. Softw. Eng. Methodology, vol. 21, no. 2, pp. 13:1-13:41, 2012.
M. Gogolla, M. Kuhlmann, and L. Hamann, "Consistency, independence and consequences in UML and OCL models," in Proc. Int. Conf. Tests Proofs, 2009, pp. 90-104.
M. Gogolla, L. Hamann, and M. Kuhlmann, "Proving and visualizing OCL invariant independence by automatically generated test cases," in Proc. 4th Int. Conf. Tests Proofs, 2010, pp. 38-54.
N. Przigoda, R. Wille, and R. Drechsler, "Leveraging the analysis for invariant independence in formal system models," in Proc. Euromicro Conf. Digital Syst. Design, 2015, pp. 359-366.
K. R. Apt and M. Wallace, Constraint Logic Programming Using ECLiPSe. Cambridge, U.K.: Cambridge Univ. Press, 2007.
P. V. Hentenryck, Y. Deville, and C.-M. Teng, "A generic arc-consistency algorithm and its specializations," Artif. Intell., vol. 57, no. 2, pp. 291-321, 1992.
M. Balaban and A. Maraee, "Finite satisfiability of UML class diagrams with constrained class hierarchy," ACM Trans. Softw. Eng. Methodology, vol. 22, no. 3, 2013, Art. no. 24.
M. Gogolla and M. Richters, "Expressing UML class diagrams properties with OCL," in Object Modeling with the OCL, The Rationale Behind the Object Constraint Language, Berlin, Germany: Springer, 2002, pp. 85-114.
C. Choi, W. Harvey, J. H. M. Lee, and P. Stuckey, "Finite domain bounds consistency revisited," in Proc. Australasian Joint Conf. Artif. Intell., 2006, pp. 49-58.
E. Torlak and D. Jackson, "Kodkod: A relational model finder," in Proc. 13th Int. Conf. Tools Algorithms Construction Anal. Syst., 2007, pp. 632-647.
N. Een and N. Sorensson, "An extensible SAT-solver," in Proc. Int. Conf. Theory Appl. Satisfiability Testing, 2003, pp. 502-518.
D. Jackson, Software Abstractions: Logic, Language, and Analysis. Cambridge, MA, USA: Press, 2006.
K. Apt, Principles of Constraint Programming. Cambridge, U.K.: Cambridge Univ. Press, 2003.
H. Bagheri and S. Malek, "Titanium: Efficient analysis of evolving Alloy specifications," in Proc. 24th ACM SIGSOFT Int. Symp. Found. Softw. Eng., 2016, pp. 27-38.
N. Macedo, T. Jorge, and A. Cunha, "A feature-based classification of model repair approaches," IEEE Trans. Softw. Eng., 2016. [Online]. Available: http://ieeexplore.ieee.org/document/ 7605502/
B. Baudry, S. Ghosh, F. Fleurey, R. B. France, Y. L. Traon, and J.-M. Mottu, "Barriers to systematic model transformation testing," Commun. ACM, vol. 53, no. 6, pp. 139-143, 2010.
M. Cadoli, D. Calvanese, G. D. Giacomo, and T. Mancini, "Finite model reasoning on UML class diagrams via Constraint Programming," in Proc. Congress Italian Assoc. Artif. Intell., 2007, pp. 36-47.
M. Clavel, M. Egea, and M. A. G. de Dios, "Checking unsatisfiability for OCL constraints," Eur. Assoc. Softw. Sci. Technol., vol. 24, doi: http://dx.doi.org/10.14279/tuj.eceasst.24.334, 2009.
A. Queralt, A. Artale, D. Calvanese, and E. Teniente, "OCL-Lite: Finite reasoning on UML/OCL conceptual schemas," Data Knowl. Eng., vol. 73, pp. 1-22, 2012.
A. D. Brucker and B. Wolff, "HOL-OCL: A formal proof environment for UML/OCL," in Proc. Theory Practice Software 11th Int. Conf. Fundam. Approaches Softw. Eng., 2008, pp. 97-100.
T. Nelson, D. J. Dougherty, K. Fisler, and S. Krishnamurthi, "Toward a more complete Alloy," in Proc. Int. Conf. Abstract State Machines Alloy, B, VDM, Z, 2012, pp. 136-149.
A. Shaikh, R. Clariso, U. K. Wiil, and N. Memon, "Verificationdriven slicing of UML/OCL models," in Proc. IEEE/ACM Int. Conf. Automated Softw. Eng., 2010, pp. 185-194.
J. Seiter, R. Wille, M. Soeken, and R. Drechsler, "Determining relevant model elements for the verification of UML/OCL specifications," in Proc. Design Automation Test Eur. Conf. Exhib., 2013, pp. 1189-1192.
N. Rosner, J. P. Galeotti, C. L. Pombo, and M. F. Frias, "ParAlloy: Towards a framework for efficient parallel analysis of Alloy models," in Proc. Int. Conf. Abstract State Machines, Alloy, B and Z, 2010, pp. 396-397.
N. Rosner, J. H. Siddiqui, N. Aguirre, S. Khurshid, and M. F. Frias, "Ranger: Parallel analysis of Alloy models by range partitioning," in Proc. 28th IEEE/ACM Int. Conf. Automated Softw. Eng., 2013, pp. 147-157.
I. Feinerer, G. Salzer, and T. Sisel, "Reducing multiplicities in class diagrams," in Proc. Int. Conf. Model Driven Eng. Languages Syst., 2011, pp. 379-393.
M. Balaban and A. Maraee, "Simplification and correctness of UML class diagrams-focusing on multiplicity and aggregation/ composition constraints," in Proc. Int. Conf. Model Driven Eng. Languages Syst., 2013, pp. 454-470.
M. Soeken, R. Wille, and R. Drechsler, "Towards automatic determination of problem bounds for object instantiation in static model verification," in Proc. 8th Int. Workshop Model-Driven Eng. Verification Validation, 2011, Art. no. 2.
N. Bjørner, N. Tillmann, and A. Voronkov, "Path feasibility analysis for string-manipulating programs," in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., 2009, pp. 307-321.
J. P. Galeotti, N. Rosner, C. G. L. Pombo, and M. F. Frias, "TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds," IEEE Trans. Softw. Eng., vol. 39, no. 9, pp. 1283-1307, Sep. 2013.
Y. Choi and M. Heimdahl, "Model checking software requirement specifications using domain reduction abstraction," in Proc. 18th IEEE Int. Conf. Automated Softw. Eng., 2003, pp. 314-317.
E. Clarke, et al., "Abstraction and counterexample-guided refinement in model checking of hybrid systems," Int. J. Foundations Comput. Sci., vol. 14, no. 04, pp. 583-604, 2003.