Model driven engineering (MDE) approaches necessitate veri cation and validation (V&V) of the models used. Balancing usability of modeling languages with veri ability of the speci cation presents several challenges. We present an approach and early results using the Semantics of Business Vocabulary and Business Rules (SBVR) standard as modeling notation and answer set programming (ASP) logic paradigm for veri cation of domain models as an attempt to address these challenges, illustrated in the problem context of regulatory compliance for business enterprises with an example from a real-life regulation.
MDE seeks to enable development of large, complex systems using models as basis, necessitating V&V of the models. The vocabulary and business rules of the problem domain need to be captured as the rst step in model building. It is desirable that models are populated directly by subject matter experts (SMEs) to minimize errors and provide them with greater control over the speci cation. Usability and veri ability are therefore two key requirements from modeling languages. In practice, we nd that modeling languages that are easy to use by SMEs are less formal, therefore harder to verify e.g. Uni ed Modeling Language (UML), while formal modeling languages such as Alloy, Kodkod, CSP, and SAT speci cation languages that have automated solvers available are hard for SMEs to use. Models facilitate V&V since they can be used to generate the formal speci cation for validating themselves that can be solved using o -the-shelf solvers as in [GD17, ABGR07, CCR08, FSB04, FF08].
In our earlier work we built a generic MDE framework for rule checking that we applied to the complex real-world problem of regulatory compliance by enterprises [RSKK17]. Our framework illustrated in Figure 1 comprises three parts: a) automated extraction from natural language (NL) text of regulations to aid SMEs in authoring a model of regulation rules [RSKK17], b) model-based generation of formal logic speci cation of rules [KSK17] and extraction of relevant enterprise data, and c) automated checking of extracted data for rule compliance using an o -the-shelf rule engine. V&V of the models used was not dealt with in this work, and is the focus of the current paper.
Direct derivation of formal logic rules from NL regulation text is not feasible [LN13], therefore controlled natural language (CNL) and a rule model are selected as logical intermediate steps. Attempto Controlled English is a CNL that translates directly to formal speci cation while we need the intermediate model for step b). We choose the SBVR modeling standard by Object Management Group (OMG) to build the rule model since SBVR a) is an expressive notation for modeling business vocabulary and rules of any domain and b) provides a CNL interface called SBVR Structured English (SBVR SE) usable by SMEs to populate the model that is grounded in rst-order logic (FOL).
Automated validation of models created using a exible CNL notation such as SBVR SE however poses several problems. SAT solvers used in existing model validation approaches [GD17, ABGR07, FSB04, FF08] use programming paradigms that are much less expressive than SBVR and do not support aggregates, relations, or functions. Alloy, Kodkod, and Object Control Language (OCL) support encoding of aggregates, relations and constraints but not of rules with modalities such as obligations and permissions, and default behavior with exceptions, all of which frequently occur in real-world problem contexts such as regulation, NLP+ML extraction 1 Model Legal text Population
of regulation
MDE framework SBVR model of regulation We extend our earlier developed MDE framework to generate the formal logic speci cation for V&V of the SBVR model in the ASP paradigm, as shown in Figure 1. Model veri cation seeks to check that the model does what it is expected to do, usually through an implementing program1. We propose inconsistency checking, scenario generation, and testing using a standard set of test cases and test data as veri cation techniques in our approach.
The objective of model validation is to ascertain that the model is a faithful representation of the problem space it represents1. We implement validation by having SMEs certify scenarios generated from the model for validity and coverage. We brie y touch upon the SBVR and ASP technologies before explaining the approach using an illustration from the KYC regulation for Indian banks. KYC is an anti-money laundering regulation that lays down guidelines for acceptance of new customers including risk categorization and identi cation procedures. 2.1
SBVR is a fact-oriented modeling notation [Nij07] that encodes rules as logical formulations over fact types that are relations between concepts2. Rules are stated in SBVR SE to populate the model. Listing 1 shows a few SBVR SE rules from the KYC example. Rules r6 and r7 de ne obligations on the bank to open an account for a customer. Rule r6 is populated in the 1http://www.inf.ed.ac.uk/teaching/courses/pm/Note16.pdf 2https://www.omg.org/spec/SBVR/1.3 Listing 1: Section of SBVR SE Rules from the KYC Example r u l e r 1 I t i s n e c e s s a r y t h a t c u s t o m e r @ i s h i g h R i s k C u s t j j c u s t o m e r @ i s l o w R i s k C u s t r u l e r 2 I t i s n e c e s s a r y t h a t c u s t o m e r @has s o u r c e O f W e a l t h E a s i l y I d e n t i f i e d i f c u s t o m e r @ i s l o w R i s k C u s t r u l e r 4 I t i s n e c e s s a r y t h a t c u s t o m e r @ i s s a l a r i e d j j c u s t o m e r @ i s g o v t D e p t i f c u s t o m e r @has s o u r c e O f W e a l t h E a s i l y I d e n t i f i e d r u l e r 6 I t i s o b l i g a t o r y t h a t bank @ o p e ns A c c o u n t F or c u s t o m e r i f bank @ v e r i f i e s I d e n t i t y O f c u s t o m e r r u l e r 7 I t i s o b l i g a t o r y t h a t bank n o t @ o p e n sA c c o u n t F or c u s t o m e r i f c u s t o m e r @ a p p r o a c h e s bank && c u s t o m e r @ i s bannedCustomer r u l e r 8 I t i s n e c e s s a r y t h a t bank @ v e r i f i e s I d e n t i t y O f c u s t o m e r i f c u s t o m e r @ a p p r o a c h e s bank && c u s t o m e r @ s u b m i t s document 2.2
ASP We select ASP for automated veri cation since it a) is a powerful, highly expressive logic programming notation supporting aggregates, functions, and optimizations and b) maps directly onto SBVR's fact-oriented model and underlying rst-order logic formalism.
Rules in SBVR are translated as rules in ASP of the form Head :- Body, where Body is the antecedent that implies the consequent Head. Statement-type rules without antecedents are translated as constraints i.e. rules with empty head, as :- Body. Relations in SBVR become predicates in ASP, with related concepts as arguments referred by their ids e.g. bank @opensAccountFor customer becomes opensAccountFor(BankId,CustomerId). Our model-based generator uses Eclipse Modeling Framework (EMF) generated model traversal functions to traverse the SBVR model and translate it to ASP rules and constraints. Listing 2 shows a fragment from the ASP program generated for the KYC example.
Listing 2: ASP Fragment for KYC Example h i g h R i s k C u s t ( C us tom er Id ) v l o w R i s k C u s t (
Cu st om erI d ) : c u s t o m e r ( Cu st om erI d ) . s o u r c e O f W e a l t h E a s i l y I d e n t i f i e d ( C ust om er Id ) : l o w R i s k C u s t ( C us to me rId ) . s a l a r i e d ( C us tom er Id ) v govtDept ( Cu st ome rI d ) : s o u r c e O f W e a l t h E a s i l y I d e n t i f i e d ( Cu st om erI d ) . opensAccountFor ( BankId , C us tom er Id ) :
v e r i f i e s I d e n t i t y O f ( BankId , Cu st om erI d ) . opensAccountFor ( BankId , C us tom er Id ) : a p p r o a c h e s ( CustomerId , BankId ) , bannedCustomer ( C ust om er Id ) . v e r i f i e s I d e n t i t y O f ( BankId , Cu st om erI d ) : a p p r o a c h e s ( CustomerId , BankId ) , s u b m i t s ( CustomerId , DocumentId ) . s u b m i t s ( CustomerId , DocumentId ) : s a l a r i e d ( Cu st om erI d ) , l e t t e r O f I d e n t i t y F r o m C o r p o r a t e ( DocumentId ) .
ASP supports encoding of extended logic programs with choice, cardinality, classical negation, and disjunction in the head of rules, not supported by normal logic programs, enabling veri cation of these features that are supported in SBVR SE. Disjunction in rule heads is a powerful feature used to model mutually exclusive paths, such as high and low risk categorization in rule r1 and and two types of low risk customers in rule r4 in Listing1. Classical negation allows explicit statement or derivation of negative knowledge, e.g. rule r7 in Listing1.
ASP solvers perform automated analysis by grounding the program i.e. generating variable-free rules given a set of ground facts and using techniques similar to SAT solving to generate solutions or answer sets of the program. 2.3
We use the DLV system [LPF+06] as the solver for our generated ASP programs. The solver performs consistency checking of the rule base, indicating con icting rules or constraints and generating answer sets for paths where no con icts exist. Answer sets by de nition are minimal, i.e. no answer set can be contained in another [Lif08], and represent the minimal set of unique scenarios for the input model. These are presented to SMEs to check whether the generated scenarios are valid and whether all important scenarios have been covered.
The KYC program of Listing2 generates four answer sets corresponding to two risk categories and four customer types. Listing3 shows ground facts provided for a single customer with id 301 and a sample answer set for salaried customer.
Listing 3: Input Ground Facts and Sample Answer Set % Ground F a c t s : c u s t o m e r ( 3 0 1 ) . a p p r o a c h e s ( 3 0 1 , 2 0 1 ) . l e t t e r O f I d e n t i t y F r o m C o r p o r a t e ( 4 0 1 ) . %bannedCustomer ( 3 0 1 ) . % S o l u t i o n s : f c u s t o m e r ( 3 0 1 ) , a p p r o a c h e s ( 3 0 1 , 2 0 1 ) , l e t t e r O f I d e n t i t y F r o m C o r p o r a t e ( 4 0 1 ) , l o w R i s k C u s t ( 3 0 1 ) , s o u r c e O f W e a l t h E a s i l y I d e n t i f i e d ( 3 0 1 ) , s a l a r i e d ( 3 0 1 ) , s u b m i t s ( 3 0 1 , 4 0 1 ) , v e r i f i e s I d e n t i t y O f ( 2 0 1 , 3 0 1 ) , opensAccountFor ( 2 0 1 , 3 0 1 ) g Although minimal, number of answer sets can grow combinatorially with conditions and ground instances. To constrain number of scenarios, only critically important conditions are modeled as disjunctions that create independent scenarios for each condition, while non-critical conditions such as id proof submitted by a customer e.g. letterOfIdentityFromCorporate are modeled as normal clauses and minimal number of ground facts are provided to prevent combinatorial explosion.
Another veri cation step is testing the ASP program using a set of manually created positive and negative test cases with test data provided as ground facts and checking generated scenarios against expected results. When test data in the form of ground fact bannedCustomer(301) is added, rule r7 becomes true, con icting with rule r6 and displays the inconsistency as shown in Listing 4.
Listing 4: Inconsistencies Shown by ASP Solver % F a c t s d e r i v e d a s t r u e i n e v e r y answer s e t : opensAccountFor ( 2 0 1 , 3 0 1 ) . % I n c o n s i s t e n c i e s : : opensAccountFor ( 2 0 1 , 3 0 1 ) .
Inconsistencies need to be corrected in the model and solutions re-generated iteratively until no anomalies remain. 2.4
In our experience of using our framework over two years on sections from three real-life regulations, we trained several groups of SMEs who found SBVR SE to be an easily usable notation to understand and specify rules without requiring knowledge of underlying technologies. Using a general-purpose CNL and model saves us the e ort of implementing a DSL, also keeps the approach generic and usable for any problem domain. CNL being more exible, veri cation is harder than in case of a DSL. Our SBVR SE language implementation therefore places some restrictions on sentence structure and keywords for ease of veri cation, taking care not to compromise on feature support.
It is desirable that V&V ensures that speci ed rules form a correct inferencing hierarchy. Work to supplement the approach described here with static analysis of the model to ag rules that are not explicated further as possible cases of missing rules, check for cycles and reachability is ongoing. However the same clause may get speci ed in multiple ways. The extra work to be performed for veri cation is compensated by other advantages of the SBVR-ASP combination mentioned earlier, also minimal translation e ort from SBVR to ASP. Not having to implement an input DSL that reduces the development and testing e ort on language engineering and model transformations. SBVR helps identify and map to actual data if available, else generate mock data in our framework [RSKK17].
Having so far worked with partial regulations, we plan to encode a few complete regulations that specify rules at di erent levels of abstraction in order to test adequacy of the SBVR and ASP notations. 3
Conclusion Usability and veri ability of modeling languages are both critical in any MDE approach, however often con ict in practice. We proposed using CNL as a stepping stone to populate models and reviewed the challenges faced in veri cation of such a model using commonly used model checking languages. We described our V&V approach using SBVR and ASP to address these challenges and illustrated it with an example from the KYC regulation for Indian banks. Ongoing investigations include managing con icts between rules using priorities and automated generation of positive and negative ground data for veri cation. 4