“If you cannot find the truth right where you are, where else do you expect to find it?”
Dōgen Zenji
Summary
Software engineering models can be regrouped in two categories depending on their target: analysis models represent business context and concerns, design ones represent systems components. Whatever the terminologies, all models are to be verified with regard to their intrinsic qualities, and validated with regard to their domain of discourse, respectively business objects and activities (analysis models), or software artifacts (design models).
Checking for internal consistency is arguably straightforward as proofs can be built with regard to the syntax and semantics of modeling (or programming) languages. Things are more complicated for external consistency because hypothetical proofs would have to rely on what is known of the business domains, whose knowledge is by nature partial and specific, if not hypothetical. Nonetheless, even if general proofs are out of reach, the truth of models can still be disproved by counter examples found among the instances under consideration.
Domains of Discourse: Business vs Engineering
With regard to systems engineering, domains of discourse cover artifacts which are, by “construct”, fully defined. Conversely, with regard to business context and objectives, domains of discourse have to deal with instances whose definitions are a “work in progress”.
That can be illustrated by analysis models, which are meant to translate requirements into system functionalities, as opposed to design ones, which specify the corresponding software artifacts. Since software artifacts are supposed to be built from designs, checking the consistency of the mapping is arguably a straightforward undertaking. That’s not the case when the consistency of analysis models has to be checked against objects and activities identified by business’ domains of discourse, possibly with partial, ambiguous, or conflicting descriptions. For that purpose some logic may help.
Flat Models & Logic
Business requirements describe objects, events, and activities, and the purpose of modeling is to identify those instances and regroup them into subsets built according to their features and relationships.
As far as models make no use of abstractions (“flat” models), instances can be organized using basic set operators and epistemic (i.e relating to the degree of validation) constraints with regard to existence (m/d), uniqueness (x/o), and change (f/m):
Using the EU-Rent Car example:
- Rental cars are exclusively and definitively partitioned according to models (mxf).
- Models are exclusively partitioned according to rental group (mxm), and exclusively and definitively according body style (mxf).
- Rental cars are partitioned by derivation (/) according to group and body style.
Such models are deemed to be consistent if all instances are consistently taken into account.
Flat Models External Consistency
Assuming that models backbone can be expressed logically, their consistency can be formally verified using a logical language, e.g Prolog.
To begin with, candidate subsets are obtained by combing requirements for core modeling artifacts expressed as predicates (21 for descriptions of actual objects, 121 for descriptions of actual locations, 20 for descriptions of symbolic ones, 22 for descriptions of symbolic partitions), e.g:
- type(20, manufacturer).
- type(21, rentalCar).
- type(22, carModel).
- type(22, rentalGroup).
- type(22, bodyStyle).
- type(121, depot).
Partitions and functional connectors (220 for symbolic reference, 222 for partitions, 221 for actual connection), e.g:
- connect(222, rentalCar,carModel, mxf).
- connect(222, carModel, group, mxm).
- connect(222, carModel, bodyStyle,mxf).
- connect(220, manufacturer_, carModel, manufacturer, mof).
- connect(121, location, rentalCar, depot, mxt)
Finally, features and structures (320 for properties, 340 for operations), e.g:
- feature(340, move_to, depot).
- feature(320, address).
- feature(320, location).
- member(manufacturer,address,mom).
- member(rentalCar,location,mxm).
- member(rentalCar,move_to,mxm).
Those candidate descriptions are to be assessed and improved by applying them to sets of identified occurrences taken from requirements. The objective being to map each instance to a description: instance(name, term()), e.g:
- instance(sedan,carModel(f1(F1),f2(F2))).
- instance(coupe,carModel(f1(F1),f2(F2))).
- instance(ford, manufacturer(f6(F6),f7(F7))).
- instance(focus, rentalCar(f6(F6),f7(F7))).
- instance_(manufacturer_,focus,ford).
Using a logical interpreter, validation can then be carried out iteratively by looking for counter examples that could disprove the truth of the representations:
- All instances are taken into account: there is no instance N without instance(N,Structure).
- Logical consistency: there is no instance N with conflicting partitioning (native and derived).
- Completeness: there is no instance type(X,N,T(f1,f2,..)) with undefined feature fi.
- Functional consistency: there is no instance of relation R (native and derived) without a consistent type relation(X, R, Origin, Destination, Epistemic) .
It must be noted that the approach is not limited to objects and is meant to encompass the whole scope of requirements: actual objects, symbolic representations, business logic, and processes execution.
Multilevel Models: From Partitions to Sub-types
Flat models fall short when specific features are to be added to the elements of partitions subsets, and in that case sub-types must be introduced. Yet, and contrary to partitions, sub-types come with abstractions: set within a flat model (i.e without sub-types), Car model fully describes all instances, but when sub-types sedan, coupe, and convertible are introduced, the Car model base type is nothing more than a partial (hence abstract) description.
Whereas that difference may seem academic, it has direct and practical consequences when validation is considered because consistency must then be checked for every level, concrete or abstract.
LSP & External Consistency
As it happens, the corresponding problem has been tackled by Barbara Liskov for software design: the so-called Liskov substitution principle (LSP) states that if S is a sub-type of T, then instances of T may be replaced with instances of S without altering any of the desirable properties of the program.
Translated to analysis models, the principle would state that, given a set of instances, a model must keep its consistency independently of the level of abstraction considered. As a corollary, and assuming a model abides by the substitution principle, it would be possible to generalize the external consistency of a detailed level to the whole model whatever the level of abstraction. Hence the importance of compliance with the substitution principle when introducing sub-types in analysis models.
Applying the Substitution Principle to Analysis Models
Abstraction is arguably the essence of requirements modeling as its purpose is to bring specific and changing concerns under a common, consistent, and lasting conceptual roof. Yet, the two associated operations of specialization and generalization often receive very little scrutiny despite the fact that most of the related pitfalls can be avoided if the introduction of sub-types (i.e levels of abstraction) is explicitly justified by partitions. And that can be achieved by the substitution principle.
First of all, and as far as requirements analysis is concerned, sub-types should only to be introduced for specific features, properties or operations. Then, epistemic constraints can be used to tally the number of specialized instances with the number of generalized ones, and check for the possibility of functional discrepancies:
- Discretionary (or conditional or non exhaustive) partitions (d__) may bring about more instances for the base type (nb >= ∑nbi).
- Overlapping (or duplicate or non isolated) partitions (_o_) may bring about less instances for the base type (nb <= ∑nbi).
- Assuming specific features, mutable (or reversible) partitions (__m) means that features may differ between level; otherwise (same features) sub-types are not necessary.
Using a Prolog-like language, the only modification will concern the syntax of predicates, with structures replaced by lists of features:
- type(20, manufacturer,[f6,f7]).
- type(21, rentalCar,[f5]).
- type(22, carModel,[f1,f2]).
- type(22, rentalGroup,[f9]).
- type(22, bodyStyle,[f8]).
- type(20, bodyStyle:sedan, [f11,f12]).
- type(20, bodyStyle:coupe, [f13]).
- type(20, bodyStyle:convertible, [f14]).
- type(121, depot,[f10]).
The logical interpreter could then be used to map the sub-types to partitions and check for substitution.
Further Reading
- Languages & Models
- Partitions
- Powertypes
- Specialization vs Generalization
- Specialization Patterns
- Connector Patterns
- External Consistency
- Shadow Models
- Quality Management
- Case study: EU-Rent Car (SBVR)