Trust by design – in praise of modularization: a case study Peter Fettke1,2[0000−0002−0624−4431] and Wolfgang Reisig3[0000−0002−7026−2810]
arXiv:2606.16670v1 [cs.SE] 15 Jun 2026
1
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany [email protected] 2 Saarland University, Saarbrücken, Germany 3 Humboldt-Universität zu Berlin, Berlin, Germany [email protected]
Abstract. Ensuring that collective adaptive systems remain safe, reliable, and trustworthy requires measures that transcend so far established formal methods, and in particular established verification techniques. In this contribution, we suggest three such measures: (1) conceptual means: runs with locally confined cause and effect of events, (2) temporal logic like verification techniques that respect and exploit such runs, (3) composing system properties from properties of components. This contribution presents a case study which particularly focuses on the benefits of modularization for achieving trust by design. Further work will develop a full-fledged theory for the presented ideas. Keywords: theory of modeling · verification · behavior modeling · predicate logic · composition calculus · Petri nets
1
Introduction
In collective adaptive systems, the interplay between software components, AIbased techniques, and human actors can produce emergent behaviors that are challenging to predict and analyze. Ensuring that these systems stay safe, reliable, and trustworthy requires methods that go beyond currently established formal methods and verification techniques. In this paper, we highlight modularity as a key to creating trustworthy systems and system models. Not only should systems be built from modules, but each single system run and each correctness argument should also follow this concept. Conceptually, all models of systems, runs, and correctness arguments share the same kind of modular structure of modules and their composition. They intertwine, yielding easy-to-comprehend models. Here, we do not present a fully developed theory of modular system construction, but illustrate the decisive concepts and their harmonic interplay through a case study. Section 2 presents the case study informally: the refund department of a company. Section 3 models several runs of the refund department. The different modules of the refund department are introduced in Section 4. Proper termination of the system is shown in Section 5. Section 6 verifies the
2
P. Fettke, W. Reisig
constraints, which are informally introduced in Section 2. The paper closes with a discussion of related work and an outlook on further research questions.
2
The running example: a refund department
The running example of this contribution is a model of the refund procedure of a retail company. The refund department processes customer refund requests (claims). Each claim involves a customer and an item, and is handled by a company staff member, who either approves or rejects it. This process is governed by several constraints: 1. Specialized staff : For each article a, there is a designated set of staff, f (a), authorized to handle claims related to a. Every incoming request a is assigned to a staff member from the set f (a). 2. Conflict of interest: Staff members may also be customers of the retail company. It must be strictly ensured that no staff member processes their own claim. 3. Limited replacement: The assigned staff member may be replaced by any other authorized staff member. For each claim, this may happen at most once. 4. Proper termination: Each customer claim is ultimately either accepted or rejected. Fig. 1 shows a model of the refund department’s behavior. This model is not very understandable; the observer of this model must himself find a structure and an order of the involved events. Furthermore, it is not obvious that the above constraints are satisfied. In the sequel, we develop this model clearly, systematically, and in a structured manner that is easy to understand. We start with the most abstract perspective, as shown in Fig. 2: Over its left interface, the refund department receives claims; over its right interface, the refund department approves or rejects claims. The boxes indicate that the department interacts with its environment through activities (Petri net transitions), i.e., in handshake mode.
refund department
receive claim
select decider (c, a) claim received
(c, a)
e f(a) e ≠c
approved claim
approve
(c, a, e)
(c, a) replacement offers (c, a, e)
d f(a) d ≠c skip offer
d e
approve claims
(c, a)
chosen (c, a,deciders d)
replace decider
e
rejected claim (c, a)
e
e1 e2 e3 idle staff
reject
Fig. 1. The refund department’s bshavior in detail
reject claims g
Trust by design – in praise of modularization: a case study
receive claims
3
refund dept approve claims
reject claims
Fig. 2. Abstract view on the refund department refund dept
receive claim
start claims A
A
choose deciders D
claims claims received received
decide claims
replace deciders
chosen chosen deciders deciders
approved approved claims claims
idle staff
approve claim
chosen deciders
rejected rejected claims claims idle staff
inform approvals
inform rejections reject claim
idle staff
Fig. 3. The six modules of the refund department
Fig. 3 refines this model by illustrating the internal structure of the refund department, which includes six modules. The interfaces of these modules include the activities of Fig. 2, as well as predicates that may apply to claims, deciders, staff, etc., represented by ellipses. Interestingly, the left and right interfaces of the replace deciders module include the same predicates.
3
Runs (behaviors) of components of the refund department
sorts: staff = {e1, e2, e3} customers = staff ∪ {c1, c2} articles = {a1, a2}
function f: articels -> sets of staff f(a1 ) = {e1, e2} f(a2) = {e2, e3}
derived sort: claims = customers articels
predicates and their types claims received: claims claims with deciders: claims staff replacement offers: claims staff idle staff: staff approved claims: claims rejected claims: claims
Fig. 4. Sets and functions of a given refung procedure
4
P. Fettke, W. Reisig run 1 choose decider
receive claim
(c1, a1)
run 1 replace decider
select decider
run 1 start claim claim received
(c1, a1, e1)
(c1, a1) claim received idle staff
claim with decider
decline replacement offer
e1
(c1, a1, e1) replacement offer
run1 decide claim approved claims (c1, a1)
approve (c1, a1, e1) claims with deciders
(c1, a1, e1)
claims with deciders
(c1, a1, e1) replacement offer
run1 inform approval approved claims (c1, a1)
inform approval of claim
e1 idle staff
(a) runs of modules of Fig. 3
claim received
receive claim
idle staff
select decider
replacement offer
run 1
approve
(c1, a1, e1)
(c1, a1)
e1
claim with decider
inform approval of claim
(c1, a1) approved claims
(c1, a1, e1)
decline replacement offer
e1
idle staff
(b) the run run1 =def run1 start claim • run1 chose decider • run 1 replace decider • run 1 decide claim • run 1 inform approval
Fig. 5. A run of a refund department
Before discussing behavioral aspects, we examine a typical example of a refund department, as shown in Fig. 4. There, we have three staff members, five customers, two articles, and a function f that assigns each article a set of staff. Classical models of discrete behavior represent single runs (behaviors) as sequences of global states and transitions between these states. The total order of steps then reflects their occurrence over time. However, there are many good reasons to order event occurrences based on causal relationships: b is ordered after a, in case b can only occur after a has occurred first. As a result, causally independent event occurrences remain unordered. It turns out that this concept aligns very well with both composition and verification. In fact, this is what Petri nets are about. Fig. 5a shows runs of some of the modules of Fig. 3: the run run1 of start claim receives a claim from customer c1 about article a1 . Run1 of choose decider selects e1 as a decider for this claim, and offers to replace e1 by some other decider. Run1 of replace decider declines this offer and remains with e1 . Run1 of decide claim approves the claim, and finally, run1 of inform approval informs the customer c1 . Fig. 5b composes those modules; yielding the run run1 : run1 =def run1 start claim • run1 chose decider • run1 replace decider • run1 decide claim • run1 inform approval
(1)
Trust by design – in praise of modularization: a case study run 2 choose decider replacement offer
receive claim
(c2, a2)
e1
idle staff
run 2 start claim claim received
(c2, a2, e1)
(c2, a2, e1)claim with decider
claim with decider
idle staff
run2 decide claim reject (c2, a2, e2)
rejected claims
rejected claims
(c2, a2)
claims with deciders
run 2 replace decider idle staff
replacement offer (c2, a2, e1)
e1 claims with deci(c2, a2, e2) ders
select decider
(c2, a2) claim received
5
(c2, a2, e1)
e2
run2 inform rejection inform rejection of claim
(c0, a0)
e2 idle staff
(a) another run of some modules of Fig. 3
idle staff
receive claim
idle staff
run 2
replacement offers c2, a2, e1
e1
select decider
claims with decider (c2, a2, e1)
(c2, a2) claim received
e1
replace decider
claims with approve decider (c1, a1, e2)
E
approved claims (c2, a2)
e2
idle staff
inform approval of claim e2
idle staff
(b) the run run2 =def run2 start claim • run2 chose decider • run 2 replace decider • run 2 decide claim • run 2 inform rejection
Fig. 6. Two other runs and their composition
Notice that in run1 , the activities decline replacement offer occurs independently from approve and inform approval of claim. As a variant of Fig. 5, Fig. 6a shows runs of the modules of Fig. 3, replacing the claim (c1 , a1 ) by (c2 , a2 ). Only the module replace decider operates differently: The decider e1 is replaced with the decider e2 . Fig. 6b composes these runs, in analogy to Fig. 5b:
run2 =def run2 start claim • run2 chose decider • run2 replace decider • run2 decide claim • run2 inform rejection
(2)
Finally, we can compose the two runs of Fig. 5b and Fig. 5a, resulting in the run of Fig. 7:
run3 =def run2 • run1 = run2 start claim • run2 chose decider • run2 replace decider • run2 decide claim • run2 inform rejection • run1 start claim • run1 chose decider • run1 replace decider • run1 decide claim • run1 inform approval
(3)
6
P. Fettke, W. Reisig run 2 choose decider
claim received
receive claim
idle staff
select decider
replacement offers
e1
select decider
c2, a2, e1
(c2, a2, e1)
(c2, a2) claim received
decline replacement offer
(c1, a1, e1)
idle staff
e1
rejected claims (c2, a2)
claims with decider (c1, a1, e2)
replace decider
inform approval of claim
(c1, a1) approved claims
replacement offer
e1
claims with decider
approve
(c1, a1, e1)
(c1, a1)
receive claim
idle staff
claim with decider
idle staff
inform approval of claim
reject e2
e2
idle staff
Fig. 7. The composition of two runs: run2 • run1 choose decider
start claim
receive claim
(c, a)
claims with deciders
select decider claims received
claims received
(c, a)
e f(a) e ≠c
(c, a, e)
replacement offers
claims with deciders
replace decider
(c, a, e)
replacement offers
d f(a) d ≠ c replace decider
c variables c: customers a: articels d, e: staff
decline offer e
decide claim approve
e1 e2 e3
approved claims
approved claims
inform approval
rejected claims
rejected claims
inform rejection
(c, a)
(c, a)
idle staff
(c, a, d)
d
e
e1 e2 e3 idle staff
approve claim
claims with deciders
e1 e2 e3 idle staff
e
(c, a)
reject claim
reject
Fig. 8. The behavior of the five modules of the refund department
This run is a run of the system of Fig. 1. The order of composition of the modules of the above run is not fixed. For example, run1 start claim and run2 start claim may be swapped.
4
A Heraklit model of components of the refund department
The instance of a refund department as in Fig. 1 yields already a bunch of runs; Figs. 5-7 show only a few of them. We strive at a finite representation of all of them, in an automaton like fashion. Fig. 8 shows such a representation as a high-level Petri net. The essential aspect are the variables c, a, d, and e. Their valuation with a customer, an article, and staff then yields runs of the modules of Fig. 4. For instance, the runs of Fig. 5 are gained as follows: 1. Module start claim: The transition receive claim can occur at any time, instantiating the variables c and a by a concrete client, for instance c1 , and
Trust by design – in praise of modularization: a case study
7
signature : sort symbols: customers articles staff variables c: customers a: articels d, e: staff
derived sort symbol: claims = customers articles
constant symbol M: set of staff
function symbol f: articels -> sets of staff
predicate symbols claims received: claims claims with deciders: claims staff replacement offers: claims staff idle staff: staff approved claims: claims rejected claims: claims
Fig. 9. The signature of the refund department
a concrete article, for instance a1 , yielding the tuple (c1 , a1 ) at the predicate claims received. 2. Module choose decider : With the tuple (c1 , a1 ) at the predicate claims received, and the authorized staff member e1 ∈ f (a1 ), occurrence of the transition select decider yields the token (c1 , a1 , e1 ) at the predicate chosen decider, and another copy of this token at the predicate replacement offers. Alternatively, the decider e2 or e3 may have been selected. 3. Module replace decider : This module substitutes the chosen decider e1 with another authorized decider, e.g. e2 . Alternatively, the transition skip offer eventually revokes the replacement offer. 4. Module decide claim: With the token (c1 , a1 , e1 ) at the place chosen decider, both transitions approve and reject are enabled, but only one of them will occur. Criteria for this choice are not modeled here. 5. Modules inform approval and inform rejection: In line with the initial module that receives the claim, these modules pass the decision on the claim to the department’s environment. Accordingly, the valuation of the variables c with c2 and a with a2 yields the runs of Fig. 6a. In this case, however, the decider e1 is replaced by the decider e2 , and the claim is approved. Composition of the modules of Fig. 8 then yields the module of Fig. 1: refund department =def start claim • choose decider • replace decider • decide claim • inform approval • inform rejection
(4)
Summing up, the runs of Fig. 5a and 6a are runs of the system modules in Fig. 8. Their respective composition show the Figs. 5b, 6b, and 7. So far, we considered the case of fixed sets of staff, customers and articles, and a fixed function f , that assigns each article a set of staff. We may generalize or abstract from these concrete sets and this concrete function, constructing a schema that allows for any such set and any such function. Technically, we construct a signature, in the framework of algebraic structures (in analogy to algebraic specification languages, such as VDM, Z, etc.). So, the signature Σ
8
P. Fettke, W. Reisig refund department
receive claim
select decider (c, a) claim received
(c, a)
e f(a) e ≠c
approved claim
approve
(c, a, e)
(c, a) replacement offers (c, a, e)
d f(a) d ≠c decline offer
d e
(c, a)
approve claims
chosen (c, a,deciders d) c replace decider
e
rejected claim (c, a)
e
elm(M) idleD staff
reject claims
reject
Fig. 10. The schema of the refund system
in Fig. 9 includes symbols for three sorts, i.e. symbols for sets of customers, articles, and staff, and a symbol for claims. Furthermore, a function symbol f is needed for the function that assigns to each article the eligible staff. The system representation of Fig. 1 almost represents also the schematic version. But there is a decisive problem: The tokens e1 , e2 , and e3 of the place idle staff must be replaced by “any staff members”. A symbol, say, M , for a set of staff does not help: considered as a Petri net token, M would be one item. Instead, idle staff (just as each other place) is a predicate that applies to the elements of (the interpretation of) M . We denote this aspect in Fig. 10 by the inscription “elm(M )” in the idle staff predicate. In formal terms, “elm” denotes the “for all” quantor. This completes the modeling of a refund department for any unspecified company. More on the formal background of the employed modeling technique can be found in [5].
5
Proper termination
As explained in Sec. 2, proper termination requires that each claim is ultimately either accepted or rejected. In technical terms, this means that whenever the transition receive claim occurs in a mode a = a0 and e = e0 (with variables a and e, an article a0 and a customer c0 ), eventually one of the transitions approve claim or reject claim occurs in the same mode. In the framework of the safety/ liveness dichotomy [2], this is a typical liveness property. Such properties are usually formulated and proven in the framework of temporal logic. We suggest a variant of temporal logic, for two reasons. As outlined in Sec. 3, we represent single runs as partially ordered sets of events rather than as sequences of events. Second, we suggest composing liveness properties of a composed system from liveness properties of its component modules. Formulated differently, we pick up “small” liveness properties directly from the structure of “small” modules and compose “large” liveness properties from corresponding properties of small modules. We exemplify this in the running example of a refund department, as in Fig. 11. In technical terms, we employ an operator “causes”, written “7→”, and formulas shaped “p 7→ q”, with propositional formulas p and q. Propositional formulae
Trust by design – in praise of modularization: a case study choose decider
start claim
receive claim
(c, a)
claims with deciders
select decider claims received
claims received
(c, a)
e f(a) e ≠c
(c, a, e)
claims with deciders
replace decider
b replacement offers
(c, a, e)
replacement offers
c decline offer e
decide claim claims approved
approve
claims approved
idle staff
(c, a, d)
d f(a) d ≠ c replace decider d
e
elm(M)
idle staff
idle staff
inform approval
approve claim
e
claims rejected elm(M)
elm(M)
(c, a)
(c, a) claims with deciders
9
e
claims rejected
inform rejection (c, a)
reject claim
reject
Fig. 11. The behavior of the five modules of the refund department
and distributed runs are closely related: Each place p is a predicate that applies to the inscribed item a; hence, p(a) is a proposition. Each transition t is assigned the predicate occurs(t), usually extended by a list of parameters. These parameters correspond to the predicates’ parameters in the environment of t. Technical details on this can be found in [6]. Here we exemplify causes properties along the running example. First, we construct for each of the six modules of Fig. 8 a cause property. Then we compose these properties, resulting in the wanted formula. The start claim module 1. occurs (receive claim (c, a)) occurrence rule of Petri nets 2. occurs receive claim(c, a)) 7→ claims received(c, a) occurrence rule of Petri nets 3. Start claim |= occurs (receive claim(c, a)) 7→ claims received(c, a) definition of the module The choose decider module 4. Idle staff.e ∧ claims received(c, a) 7→ claims with deciders(c, a, e) ∧ replacement offers (c, a, e) occurrence rule of Petri nets 5. choose decider |= Idle staff.e ∧ claims received(c, a) 7→ claims with deciders(c, a, e) ∧ replacement offers (c, a, e) definition of the module The replace decider module 6. idle staff.d ∧ claims with deciders(c, a, e) ∧ replacement offers (c, a, e) 7→ (claims with deciders(c, a, e) ∧ idle staff.d) ∨ (claims with deciders(c, a, d) ∧ idle staff.d occurrence rule of Petri nets
10
P. Fettke, W. Reisig
7. replace decider |= idle staff.d ∧ claims with deciders(c, a, e) ∧ replacement offers (c, a, e) 7→ claims with deciders(c, a, e) definition of the module The decide claim module 8. decide claim |= claims with deciders(c, a, e) 7→ (claims approved.(c, a)) ∨ (claimes rejected.(c, a)) occurrence rule of Petri nets The inform approval module 9. claims approved.(c, a) 7→ occurs (approve claim(c, a)) occurrence rule of Petri nets 10. inform approval |= claims approved.(c, a) 7→ occurs (approve claim(c, a)) definition of the module The inform rejection module 11. claims rejected.(c, a) 7→ occurs (reject claim(c, a)) occurrence rule of Petri nets 12. inform rejection |= claims rejected.(c, a) 7→ occurs (reject claim(c, a)) definition of the module Proper termination of the return department, as defined in Sec. 4, reads occurs(receive claim(c, a)) 7→ (occurs(approve claim(c, a)) ∨ occurs(reject claim(c, a))).
(5)
Validity of this formula is now gained as the composition of the above properties 3., 5., 7., 8., 10., and 12. of the six modules.
6
Verification of the constraints of Section 2
Sec. 2 presented four requirements for the refund procedure. In fact, the model in Fig. 11 meets them: – Specialized staff : This property holds obviously: for each article a, the designated set of staff, f (a), is formulated in the structure of Fig. 4. At the schematic level, in the signature of Fig. 9, is authorized to handle claims related to a. Every incoming request a is assigned to a staff member from the set f (a). – Conflict of interest: There are two transitions that assign a staff member e to a claim: select decider and replace decider. The inscriptions of both transitions require that customers are never identical with the assigned decider. – Limited replacement: The assigned staff member may be replaced by any other authorized staff member. For each claim, this may happen at most once. Transition replace decider is the only transition that generates replacement. It is geared by the token at place idle. – Proper termination: This requirement has been proven in Sec. 5.
Trust by design – in praise of modularization: a case study
7
11
Discussion, related work, and conclusions
Computer-integrated systems exhibit two faces: the technological and the applied face. Edsger W. Dijkstra has frequently suggested to strictly separate both sides and to build a “firewall” between them [4]. His justification: The methods to attack the computer scientists’ formal, mathematical “correctness problem” differ fundamentally from the methods to attack the applicants’ informal “pleasantness problem”. In this setting, a model is always confined to one side or the other of this wall. A plethora of work tackles the challenges of solving the correctness and pleasantness problem from different research communities. For example, “reactive systems” by Aceto et al. [1] from a software engineering perspective or “Conformance checking” by Carmona et al. [3] from a BPM perspective. In contrast to Dijkstra and many other approaches, we understand modeling as an activity that should allow a seamless transition between formally and informally given or asserted facts of a computer-integrated system. Technology and applications must be interlocked by shared models, based on the same foundations. As a key concept, our approach is based on a universal idea of composition. Our case study demonstrates that both sides of Dijskrta’s wall can be grounded on the same foundations. It is obvious that this approach has decisive advantages and will achieve tremendous gains: It is seamlessly possible to capture the main ideas of a natural and intuitive understanding of the world we live in, enrich this understanding with formal concepts, and use the description as a foundation for supporting development. As a central feature of our approach, we first verify the properties of the system’s components. Based on this verification, the properties of the composite system are formally derived. Future work will expand these ideas into a complete theory.
References 1. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press (2007) 2. Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985) 3. Carmona, J., van Dongen, B., Solti, A., Weidlich, M.: Conformance Checking: Relating Processes and Models. Springer (2018) 4. Dijkstra, E.W.: Reply to comments. Commun. ACM 32(12), 1414 (1989) 5. Fettke, P., Reisig, W.: Understanding the Digital World: Modeling with Heraklit. Springer (2024) 6. Reisig, W.: Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer (1999)