Abstract
Business rules control and constrain the behavior and structure of the business system in terms of its policies and principles. Business rules are restructured frequently as per the internal or external circumstances based on market opportunities, statutory regulations, and business focus. The current practice in industry, of detecting inconsistencies manually, is error prone, due to the size, complexity and ambiguity in representation using natural language.
Our work detects inconsistencies in business rules based on model checking that exploits the FOL basis of SBVR specification. We aim to reduce the burden on solvers and obtain effective system level test data, leading to the development of a novel inconsistency rule checker based on extracting the unsatisfiable cores using solvers like Z3, CVC4, etc. We introduce the concept of graphical clusters, to partition SBVR vocabularies and represent the former exploiting the many-sorted logic and graph reachability algorithm, thus reducing the domain of quantification and the number of uninterpreted functions. The translation of SBVR to SMT-LIBv2 is implemented as part of our tool BuRRiTo. Experimental results are shown on industrial level rule sets.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Sarbanes Oxley Act: Sarbanes Oxley Act. https://www.thebalance.com/sarbanes-oxley-act-and-the-enron-scandal-393497
Zeginis, C., Plexousakis, D.: Business Process Modelling. http://www.csd.uoc.gr/~hy565/lectures/Lecture-2-BP%20Modeling.pdf
Semantics of Business Vocabulary and Rules (SBVR). http://www.omg.org/spec/SBVR/. Accessed 29 Sept 2015
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org
Cok, D.R., et al.: The SMT-LIBv2 language and tools: a tutorial. Language C 2010–2011 (2011)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Chittimalli, P.K., Anand, K.: Domain-independent method of detecting inconsistencies in SBVR-based business rules. In: Proceedings of the International Workshop on Formal Methods for Analysis of Business Systems, pp. 9–16. ACM (2016)
Kendall, E., Linehan, M.H.: Mapping SBVR to OWL2. Technical report, IBM Research Report, RC25363 (WAT1303-040), March 2013
Reynares, E., et al.: SBVR to OWL 2 mappings: an automatable and structural-rooted approach. CLEI Electron. J. 17(3), 3 (2014)
Karpovič, J., et al.: The comprehensive mapping of semantics of business vocabulary and business rules (SBVR) to OWL 2 ontologies. Inf. Technol. Control 43(3), 289–302 (2014)
Karpovič, J., et al.: Experimental investigation of transformations from SBVR business vocabularies and business rules to OWL 2 ontologies. Inf. Technol. Control 45(2), 195–207 (2016)
Jackson, D.: Alloy: a Language & Tool for Relational Models (2012). http://alloy.mit.edu/alloy/applications.html
Bocic, I., Bultan, T.: Efficient data model verification with many-sorted logic (T). In: 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 42–52. IEEE (2015)
Business Rules Group: EU-Rent Car Rental case study. http://www.businessrulesgroup.org/first_paper/br01ad.htm
Glimm, B., et al.: HermiT: an OWL 2 reasoner. J. Autom. Reasoning 53(3), 245–269 (2014)
Sirin, E., et al.: Pellet: a practical OWL-DL reasoner. Web Semant. Sci. Serv. Agents World Wide Web 5, 51–53 (2007)
Cohn, A.G.: A many sorted logic with possibly empty sorts. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 633–647. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_197
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Graph algorithms. Introduction Algorithms 6 (1992)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_28
Dutertre, B., De Moura, L.: The yices smt solver. Tool Paper 2(2), 1-2 (2006). http://yices.csl.sri.com/tool-paper.pdf
Bjorner, N.: Enumeration of Minimal Unsatisfiable Cores and Maximal Satisfying Subsets. https://github.com/Z3Prover/z3/blob/master/examples/python/mus/marco.py
Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple MUSes quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160–175. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38171-3_11
Mitra, S., Chittimalli, P.K.: A systematic review of methods for consistency checking in SBVR-based business rules (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Anand, K., Chittimalli, P.K., Naik, R. (2018). An Automated Detection of Inconsistencies in SBVR-based Business Rules Using Many-sorted Logic. In: Calimeri, F., Hamlen, K., Leone, N. (eds) Practical Aspects of Declarative Languages. PADL 2018. Lecture Notes in Computer Science(), vol 10702. Springer, Cham. https://doi.org/10.1007/978-3-319-73305-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-73305-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-73304-3
Online ISBN: 978-3-319-73305-0
eBook Packages: Computer ScienceComputer Science (R0)