The highly decoupled nature of distributed systems can greatly simplify modular development. However, it is easy to lose track of component interactions and emerging system behavior. To inspect the behavior of the aggregated system, an abstract model and analysis tools can be of great help. In this paper, we present such a model that follows the Event-Driven Architecture paradigm. We argue that a Petri net model that captures the event flow, without modeling event data, is a useful abstraction to give insight into a system composed of distributed components. We present a symmetric Petri net model with publish-subscribe middleware and a generic abstraction of components. The model was designed with the intention to produce a finite P/T net to be compatible with current Petri net model checking tools. To build such a model, information about component behavior is necessary. We show that this information is encoded in the system implementation, and we describe potential means for automatic extraction. With the formal Petri net model, we enable the use of established verification methods. We discuss ideas from business process conformance checking and other verification properties that may deepen the system understanding. The proposed methods can be used either for static analysis during design time or to automatically signal issues at runtime.
A distributed system is a collaboration between multiple self-contained modules or components. Since these are usually individually developed separate code bases, this approach promotes modular development with a high focus on the individual parts.
However, hard program borders facilitate ignorance to other components and alienate developers from foreign code bases. Additionally, in the running system, components can connect and disconnect to the distributed system at any time, changing the system behavior continuously. It is hard to keep the overview in this context making predictions on the emergent system behavior exceedingly dificult. Can the required workflows be executed? Which event afects which component? A simple look at the implementation does not answer these questions and design documents and specifications also cannot consider every possible system adaptation.
However, a model of the implementation can be used in combination with a specification to answer such questions with formal verification. Yet verification can be complicated and increases development efort. To make these verification methods accessible, the implementation model should be extracted directly from the implementation. Additionally, if this model uses adequate abstractions, it stays humanly understandable, and formal methods can be used practically.
A common abstraction for distributed systems is the Event-Driven architecture paradigm (EDA). In an EDA system a central middleware connects distributed components using a standardized communication abstraction. Commonly a publish-subscribe interface is used here.
A benefit in using an EDA model to reason about the emergent system behavior is that message
contents are usually not relevant. Just knowing the event flow already gives a lot of insight,
while the precise forking conditions are often irrelevant for the general system capabilities.
Conveniently, if messages are represented by type instead of their content, messages can be
reduced to a token that is exchanged between communicating components. With this abstraction
Petri nets [
With a Petri net system model we can use diferent verification methods to compare our
model with a given specification. The specification can take many forms such as logical formulas
and other formalisms such as workflow nets (WF-nets) [
In this paper we present a Petri net model of a publish-subscribe system with a generic model
of components for verification purposes. We describe what is necessary to build the model
automatically from component implementations and give examples for usable verification methods.
In particular, we describe how a behavioral specification in form of business processes can be
integrated in the verification process by using methods from business process conformance
checking [
In the following we give an overview of our mainly used concepts to compile a verification approach for publish-subscribe systems.
In EDA, components observe events and notify other components about events using messages.
An event is a “significant change in state” [
With EDA, the computation capacity of distributed hardware can be leveraged, e.g. to run interconnected web services, or to connect physically distributed devices as in IoT applications.
Petri nets are a formalism for concurrent processes [
Transitions can consume and produce tokens on places, depending on the connecting arc direction and weight. Arcs that connect a place with a transition in the direction from to make an input place of . Similarly, if an arc connects a transition with a place , is an output place of . The set of input places of a transition is denoted by ∙ and the set of output places is denoted by ∙ . A similar notation is used for the pre- and post-sets of places.
A transition is enabled if all input places contain at least as many tokens as the arc weights specify. Enabled transitions can fire non-deterministically. A firing transition consumes tokens from the input places and produces tokens on the output places according to the arc weights.
In a system model, tokens on places represent the system state and transitions represent the state changes. P/T nets are well investigated, making them a good target for model checking.
However, in classical Petri nets, tokens are indistinguishable from each other. But, to model
systems with practical complexity it is often useful to discriminate them. Colored Petri nets
address this issue by extending Petri nets with a type (or color) for tokens [
A kind of colored Petri nets are Symmetric Petri nets (introduced as Stochastic Well-Formed
Colored Nets) defined by Chiola et al. [
Our model will follow the definition from Chiola et al. although we will abbreviate large transition patterns. In these cases we will show an example for the unabbreviated patterns. However, we observe that patterns can be unfolded into a P/T net for model-checking.
Business processes describe a collection of tasks that are used to build a product or that are
involved in a service. A business process may define a series of tasks, parallel tasks, tasks that
are executed conditionally or a combination of these options. There are a variety of business
process models [
Van der Aalst was instrumental to formalize business processes as Petri nets including the
definition of a separate net class called workflow nets [
To facilitate the understanding of business processes in WF-nets, other process models define
translations back to Petri nets [
Petri net models where used before in distributed systems. E.g.: Aldred et al. used Petri
nets to model diferent decoupling approaches in distributed systems [
Valero et al. and Gomez et al. modeled a publish-subscribe system in a timed colored Petri
net specifically for verification purposes. Their model targets web services with a focus on
message timing and timeouts [
Unfortunately, the essence of software components is vague. Szyperski et al. summarize
it as follows: “One thing can be stated with certainty: components are for composition. [...]
Beyond this trivial observation, much is unclear.” [
The EDA paradigm intrinsically exploits the composability by decoupling components [
“Underlying almost all models of concurrent systems is the assumption that an execution consists of a set of discrete events, each afecting only part of the system’s state. Events are grouped into processes, each process being a more or less completely sequenced set of events sharing some common locality in terms of what part of the state they afect. For a collection of autonomous processes to act as a coherent system, the processes must be synchronized.”
Based on the former descriptions, we define components in an EDA system as a set of processes that are executed as a reaction to incoming events. During the execution of a process, new events can be generated to synchronize component state with other components. With this definition, we can model a publish-subscribe system more precisely and use the model to improve verification accessibility and expressiveness.
An interesting verification branch uses runtime events to evaluate the system behavior. E.g.:
Schmerl et al. built a colored Petri net from runtime observations [
However, models always sufer a credibility gap. While the system implementations can deviate from manually created models, automatically discovered, log based models can always be incomplete. Also, models created by both approaches get outdated when the system evolves. This is why we like to explore system models that are close abstractions from the implementation. We aim at a model that can be automatically generated from code, to be used for verification. This approach would make model checking much more user-friendly and afordable.
In this section we introduce our Petri net model of a publish-subscribe system. We will first highlight our assumptions. After that, we break down the parts, explain their modeling and functionality. The parts are then extended with a synchronization structure for fairness constraints. At the end of this section, we describe what system information is needed to build the model and how we envision an automatic extraction from the implementation. The complete model is shown in Figure 9.
If we want to analyze the behavior of a complex distributed system, we cannot model every detail of the component implementations. Instead, we should find the right balance between abstraction and detail. Our assumptions try to balance model expressiveness and simplicity.
Given our system follows the EDA paradigm it is reasonable to orient our abstractions towards EDA principles. This means that the movement of events is a central concept. To analyze the system behavior it is not essential to know the event content, but which actions can follow. If the event content determines an event reaction, non-determinism can be used instead. Consequently, we do not model event contents, only event types.
Additionally, we use channels as event filtering mechanism [
Our model use case is to verify a specification is covered; we want to know if a specified behavior is executable in the system. Therefore, we do not model unexpected failures like e.g. link failures or message loss and target the analysis of the expected system.
Also, we only consider the known components. If previously unknown components connect to the system, the model has to be rewritten. 1 EnvEvent = ee[1-m] 2 Notification = n[1-n] 3 SubState = [true, false] 4 ComponentEvent = EnvEvent, Notification 5 AllEvents = ComponentEvent, SubEvent 6 Component = cpt[1-o] 7 Process = p[1-p] 8 Action = a[1-p]_[1-q] 9 Channel = [envch, ch[1-r]]
Finally, we exclude loops and recursive functions for publishing behavior. Although valid in EDA components, we presume that loops are used to compute values, not to communicate. With this assumption the reachability graph of component processes should be finite.
Tokens that are produced on places must satisfy a color domain which is composed of color classes, e.g.: the place (see next section) has a domain composed of two classes × . In a P/T net this composition is unfolded so that there is a place for every component-event combination.
In the implementation the color domain represents required information to execute the behavior that is molded by the consuming transitions. Following the example this would be the afected component and what event type is received.
The color classes our model is based on are shown in Figure 1. Classes can be an indexed
list of items (e.g. p[1-p] defines a list containing the processes 1 to ), a list of named items
(e.g. SubState class), or a combination of both (see [
Events are the central communication messages sent over the network. However, our usage of the term ’event’ is not equivalent to the usage in an EDA since our environment exceeds the EDA borders. We distinguish between three types of events as depicted in Figure 2a: 1. Environment events are sent between components and entities that are not part of the communication via the NoSe. 2. Subscription events are sent from components to the NoSe to update subscription states. 3. Notifications are used for intercomponent communication. They are published on a specific channel and forwarded to all channel subscribers by the NoSe. (a) Components communicate with three kinds of events: (1) environment events are used to communicate with the environment, (2) PubSubEvents are sent to the NoSe and can be a subscription update or a notification, and (3) the NoSe distributes notifications back to the components.
Events are tokens with a given type. The event type is also a placeholder for the event contents. Places holding events will unfold to at least one place for every event type.
Components interact with two main event places (see Figure 4a) and NoSeEvents. cannot be subscription updates and are always directed at a specific component. NoSeEvents can be any of the three event types and are sent from a source component. Additionally, are sent on a specific channel. If the event is a subscription, the channel is the target for the subscription update. If the event is a notification, the channel is used by the NoSe to determine the afected subscribers. If the event is an environment event, the channel should always be the special type ℎ to be consistent with the place domain. In practice this channel will not be used by the environment.
The fundamental purpose of the Notification Service (NoSe) is to forward events from one
component to other components. In a publish-subscribe system, components can subscribe
to a topic of events. The NoSe then filters all incoming events according to the subscriptions
before forwarding. There are a variety of filtering mechanisms [
Internally the Nose has to 1. track subscription states, 2. forward events to all components where the subscription filter applies, 3. drop all events where the filter does not apply, and 4. update the subscription state according to special events.
We describe this behavior as depicted in Figure 3b and 3c. The Distribute transition forwards
events of type Notificationfrom NoseEvents to all components on the DistributedEvents
place. The broadcast is modeled by using the SComponent identifier which encodes the set of
every component defined by the class (see [
ENvoeSnets Subscribe <cmpt, chnl, <cmpt, chnl, substate> subdate> cmpts.al ⨯ chnls.al ⨯ {false}
<cmsupbtd,acthen>l, D(event) = SubState substate <> subdate <cmpt, chnl, subdate>
D(event) = Notification
<cmpt, chnl, <cmpt, chnl, subdate> notification> D(event) = SubState
iver, ation> e c
fi <rec noti < Subscrl,iptioncshnnl,osnuSbusbtsactrei>ber, n r,ch te> ive sta e b rec su <
subState = true Notify Drop < nonSub subState = false notification> chnl,scriber, <receiver, chnl, notification>
< S tooennpC m , c h n l, n o it fi c a it o n >
(b) The NoSe distributes notifications to subscribers or updates subscriptions. The subscription function is idempotent.
The distribution strongly benefits from a colored Petri net approach. For every combination of sender, channel and notification type, notifications can be sent to every receiver. In an unfolded P/T net every place-transition-combination has to be instantiated, resulting in a large structure.
The transition updates the subscription state of a component if the event is of type
SubState. Additionally, the current subscription has to be diferent from the update. If so the
guard is fulfilled, a token with the old subscription state is consumed for the given component
and channel, and a new token with the new state is produced. If the subscription state is
equal to the received subscription event, the update has to be ignored so that subscriptions are
idempotent [
Connected to the NoSe are the distributed components. We put forward a pattern of how components behave in publish-subscribe systems. This pattern can be explicit or implicit, but we argue an explicit implementation is beneficial. The pattern consists of the following parts (illustrated in Figure 4a, 5a and 5b): • An initialization routine, which may or may not produce events. Often, this routine will be used to subscribe to channels. • Receiving events from other components, or the environment (e.g. a sensor or the OS). • Event deconstruction of received events to select a process as reaction or to drop the event. • And the execution of the selected Process, which may or may not produce new events.
Following this pattern a component is a collection of executable processes including one initialization routine. A component reacts to an incoming event by executing a process based on the incoming event type and content. The process execution is split into a sequence of actions that change the system state. For our Petri net model, we only consider actions that publish an event and the order in which actions can be sequenced.
Incoming events trigger a deconstruction mechanism. In the implementation this is usually a switch case equivalent. In our model the deconstruction explicitly either selects a process to react or ignores the event with two transitions.
Undefined cmpts. al > t p m c <
Process <cmpt, p>
Init initPr=oicneitsPsroces<sc(mcmpptt,)init> PrNoecxetss <cmpt, chnl, event>
NoSe
Events event ∉ mustProcess(event)
Component
Drop <cmpt, event> <cmpt, p> Deconstruct e<vcemnpt>t, p ∈ deconstruct(event)
Component
Events (a) Transitions of a component. Events are received in the ComponentEvents place and send by a process to the NoSeEvents place. Processes are selected based on incoming events by the deconstruction transition. A special init process is executed on component startup. actn ∈ endAction(cmpt, p)
End
Process actn = a[process]_1 <cmpt, p, actn>
PrSotcaertss <cmpt, p, actn> Running
<cmpt, p, post> <cmpt, p, actn> (event, chnl, post) ∈ eventAction(cmpt, p, actn)
Action
<cmpt, chnl, event> NoSe
Events (b) After it is started a process is in a running state until it finishes. A running process can change the system state with actions. Only actions that produce events are modeled. 1 NextProcess = Component x Process 2 3 Deconstruct | process ∈ deconstruct(event) 1 Undefined = Component 4 ComponentEvents.Deconstruct = <component, event> 2 5 Deconstruct.NextProcess = <component, process> 6 7 ComponentDrop | event ∈/ mustProcess(event) 8 ComponentEvents.ComponentDrop = <component, event> 3 InitProcess | initProcess = initProcess(
component) 4 Undefined.InitProcess = <component> 5 InitProcess.NextProcess = <component, initProcess> (a) Component deconstruction of incoming events.
Each event can trigger a process, be dropped or both. (b) Every component is initialized with a specific process. Only initialized components can receive events. (c) Processes are selected by the deconstruction mechanism. Each event received by a component can trigger a process as an event reaction. dropped or deconstructed non-deterministically.
The transition discards events that should be ignored. We abbreviate its guard predicate with the formula ∈/ (). To expand the formula, all cases that do not require a reaction are enumerated as shown in Figure 6b. The drop transition is enabled for all events that return for the relation.
The transition is enabled for all events that may return a process. An event can result in multiple processes non-deterministically. We abbreviate this behavior with the formula ∈ (). The formula expands to the pattern shown in Figure 6d. For every event where is , cannot be . Or ∀ ∈ : () ⇒ (). However, an event can be
During startup, a component usually initializes its state, connects to the NoSe and often subscribes to a channel. We model this behavior with the transition. Before the transition has fired, the corresponding component state is undefined, and it cannot receive events (see Section 4.7). Only after initialization, more processes can be queued. We as shown in Figure 6c. The formula defines exactly one process for each component. abbreviate the transition predicate with the formula () → A component can produce new events in processes. Figure 1 shows that processes are uniquely 1 2 3 (action = a_x1 AND postAction = a_y1 AND event = e_z1 AND channel = type1) OR (action = a_x2 AND postAction = a_y2 AND event = e_z2 AND channel = type2) OR ...
(a) Action transition pattern. 1 event != e1 AND 2 event != e2 AND 3 ... 1 (component = c1 AND init = p1) OR 2 (component = c2 AND init = p2) OR 3 ... (b) Component drop transition pattern. (c) Init process transition pattern. 1 (event = e1 AND process = p1) OR 2 (event = e1 AND process = p2) OR 3 (event = e2 AND process = p1) OR 4 (event = e2 AND process = p3) OR 5 ... identified with an ID, indicated by the class. In the model a process is gated by a start and an end transition. Between these two transitions, the process is in its running state, where a sequence of actions is executed. In the component implementation, the start transition corresponds to the function call of the given process. The guard of the start transition ensures that the first action of the given process is produced.
Each action is executed by the transition and always produces an event. Actions are indexed by a process ID and an action ID (see Figure 1). An action that produces a Notification corresponds to a call to the ℎ function in the publish-subscribe interface. An action that produces a event corresponds to a call to the or function in the publish-subscribe interface. An action that produces an EnvEvent corresponds to the part of the code that interacts with the environment.
In a custom framework it might be useful to publish environment events with the publishsubscribe interface, on the special ℎ channel, for easy parsing.
The action transition predicate generates all possible action sequences and is abbreviated with the formula (, ℎ, ) ∈ (, , ). If a process includes a condition that produces multiple event sequences, an action can produce diferent followup actions. Thus, multiple transitions are enabled non-deterministically. Consequently, the guard maps the parameters from the place domain to at least one tuple of (, ℎ, ). The expanded pattern is shown in Figure 6a
The end transition corresponds to the return statement of the function previously called with the start transition. The guard of the end transition is an enumeration of end actions abbreviated by the formula ∈ (, ). The pattern expansion is shown in Figure 6e. It is possible that and end action are simultaneously enabled to allow conditional endings of a process. However, every action sequence requires an end action as last action to ensure process termination. 1 EnvEvents = Component x EnvEvent 2 3 Sense | - // no guard 4 EnvEvents.Sense = <component, event> 5 Sense.ComponentEvents = <component, event> 6 7 EnvironmentOut | D(event) = EnvEvent 8 | channel = envch 9 NoSeEvents.EnvironmentOut = <component, channel, event> 10 11 EnvironmentIn | 12 EnvironmentIn.EnvEvents = <component, event>
The system environment contains every entity that cannot use EDA abstractions to communicate with components, e.g.: human interaction, sensors or OS events. Because it is highly individual, we make no assumptions of its behavior. However, for a basic compatibility we define a default behavior with two transitions: EnvironmentIn and EnvironmentOut . These transitions can produce and consume EnvEvents in any order; at any time.
In general each component has a unique sensing capability (e.g. a specific combination of sensors). Therefore, produced environment events always target a component. Consequently, the domain of the EnvEvents place is a tuple consisting of a produced event and a targeted component. Idle components can then sense environment events, deconstruct them and react with process actions.
For verification purposes it is useful to restrict the production of events to specific start events and collect produced events. This can be achieved by removing the EnvironmentIn transition, putting the desired start event on the EnvEvents place, and adding an output place to the EnvironmentOut transition that collects the events consumed from the NoseEvents place.
Modelling just the communication routes of our system is insuficient if events and processes have ordering constraints. To bind the arrival of an event to a process execution, we introduce a ComponentIdle place. If an event arrives via Notify or Sense, a token from the receivers ComponentIdle place is consumed. Components cannot receive new events with an empty ComponentIdle place. The ComponentEvents place is therefore safe. The StartProcess transition returns the ComponentIdle token after deconstruction, freeing the event reception. As a result, component processes can run in parallel. The execution order depends on the event arrival order. Initially the ComponentIdle place is not marked to ensure the is always started first.
Events can only accumulate in an arbitrary order in the NoSeEvents and DistributedEvents
places; the models only unbounded places (excluding environment places like EnvEvents since
the environment has no canonical form). However, often it is desirable to guarantee event
ordering constraints. A similar problem is formulated in the literature for distributed event
1 Source = Component
2 Sync = Component
3 ComponentIdle = Component
4 NoSeIdle = {}
5
6 StartProcess.ComponentIdle = <component>
7 ComponentDrop.Idle = <component>
8 ComponentIdle.Sense = <component>
9 ComponentIdle.Notify = <receiver>
10
11 Sync.Action = <component>
12 EnvironmentOut.Sync = <component>
13
14 Distribute.Source = <component>
15 Subscribe.Source = <component>
16 SubDrop.Source = <component>
1 Done = {}
2
3 Notify.Done = <{}>
4 NotifyDrop.Done = <{}>
5 Subscribe.Done = <{}>
6 SubDrop.Done = <{}>
7
8 NoseIdle.Distribute = <{}>
9 NoseIdle.SubDrop = <{}>
10 NoseIdle.Subscribe = <{}>
11
12 Resume | - // no guard
13 Resume.NoseIdle = <{}>
14 Resume.Sync = <component>
15 Source.Resume = <component>
16 Done.Resume = <{}>
systems. Muehl et. al. [
We add a synchronization mechanism between components and NoSe to ensure event ordering constraints. The NoSe can only process events if NoseIdle is marked. After the final transition has fired (i.e. Notify , Subscribe or the corresponding drop transitions) a token is produced on the place and the transition resets the event processing transitions.
The Sync place then ensures synchronization between NoSe and Components. A token is required to enable the transition. We can guarantee FIFO ordering with a Sync place domain over all , or Total ordering with a single shared token for all components. Only after the previous event has been delivered and the transition has fired the next action can produce a new event.
To guarantee Causal ordering the notification service needs to store additional information. Firstly, the past notification order, and secondly, which event was already delivered to which consumer. This would be a complex addition to the model and is therefore excluded. n o C s c<m itcoafi
n o N t Tom Meyer CEUR Workshop Proceedings n o i t a c i f i t No is =t) l,n D en ch n> ve( ,tp ito D > e t a d b u s l, n h t> taetS ,tcp p <cmp e Sub cm ro c = < D i ) b
t v en e> uS re e(vD tadb
u S l,s n h n tea et ,
c o St da tp e it Sub sub cm irb tcpm saudb a = <> < c sb < uS l, lla⨯ ll⨯ > n o e ti rop slaf ifica
D = ot r, > ifty tate nl,n pt,>lnhc,t>petmatcsbus oenD <noncShunbls,csruibbestate oN ubsS receiver,ch <cml,,cnh te> < nhc ,revi ecer < ircp,l ifto e=t s iton y true s N ta ub Sbu
s tnevEvnE =)tneve(D no ven = lennahc iv (cmp t> <hcvne n t> e ) l,veen ten <cmpt> m nt n m t n ac ch n u
, ,t iro O o p p v r t, cm En n cit l,e E At n en ch v , e t
t> ven ,e t p cm e < s n e
S t> ∈ pm p )ts c< <cm o p , l n n ch io
t ,t c n A e v e ( n e v e t t( c c ,tpp> trsoun trsunoec m c d c e ∈ < D p > t n e v e > ,t tcp<m toennp rop c< p m s> c<m(ssec c o ss tPr t n e on le p Id ,tcpm tven> < e s t s x e e c N ro
P > t s o p , p ,t p m c < m D o
C
The complete model is shown in Figure 9. For assembly, all variables need to be instantiated, i.e.: the final enumeration for all color classes (Figure 1) and the final transition guards. We distinguish between the following kind of information: Static information is encoded in the component implementations and known at compile time. For each compiled component the processes and action transitions are static. As a result the Process and classes can be enumerated completely at compile time. Additionally, initialization processes and event deconstruction is static. Consequently, the transition guards for the initProcess, deconstruct and mustProcess transition can be generated.
However, action sequences are still incomplete since the used channels and event types can depend on the component state. Hence, the remaining classes are dynamic.
Dynamic information For behavior that depends on the component state, we need assumptions or further knowledge to build the model. This knowledge might be known by the system designers or accumulated dynamically at runtime. However, newly discovered information then requires a rebuild of the model making all previous analysis obsolete.
The most characteristic dynamic information in the model are the involved components. During the system lifetime components can disconnect and entirely new components can connect. Thus, the enumeration of components in the -class changes. Newly introduced components also introduce new events and channels. This makes the Notification, EnvEvent and Channel classes also dynamic.
Furthermore, actions may change the channels on which events are published. While the domain of event types is static, channels are usually unrestricted i.e.: represented as strings. Creating an infinite number of new channels is entirely possible. Consequently, for newly introduced event-channel combination, a new action instance has to be added to the guard of the transition. If this action is also an end action, the EndProcess transition has to be updated as well. The new action instance will still have the same ID and post action. Environment Information is what interacts with the system not using a publish-subscribe interface. However, the environment transitions introduced in Section 4.6 can be replaced with a more sophisticated environment model. In this case, the environment model has to be provided for the system composition.
The Initial marking depends on the use case. Yet, the ComponentEvents place is the most noteworthy to be marked. An initial set of events can be defined here. If desired components can be individually initialized by moving tokens from the Undefinedplace to the ComponentIdle place and setting the subscription state for a set of component-channel combinations to . Additionally, the NoSeIdle place should be marked initially.
Manually collecting information that is already available in the component implementation is cumbersome and prone to errors. Instead, it is desirable to parse the implementation for information. We think this is possible with a static code analysis at compile time if the code: 1. uses a recognizable publish-subscribe-interface, 2. marks the initialization process, 3. has a deconstruction function of the form () → with parsable event cases, 4. uses the same kind of event deconstruction for environmentally caused processes, and 5. marks environment interactions in a manner that is parsable, e.g.: with an interface, structured logs or comments.
This functionality could be integrated to an existing publish-subscribe client library. Besides the already existing publish-subscribe interface, this library could export a component interface with a deconstruction function and a distinct function to send environment events. Additionally, a basic process interface could be provided to encapsulate the event reactions. Then a static code analysis has to extract the following information from the implementation for each component: 1. The process that is used for initialization. 2. All possible event-process combinations in the deconstruction routine.
3. All possible action sequences.
The initialization process can be assigned to a known variable, so it can be extracted by reading this variable.
To parse the event-process combinations the return values (started processes) of the deconstruction function have to be related to a causing event. We assume this is usually done in a switch-case block, a matching statement or similar kinds of case distinction. Given the simple form that each event is handled by one case arm and each case returns at least one process, an extraction method traverses all case arms, stores the event for each case, and adds the returned processes to the stored event.
To extract the action sequences from a process, the process implementation has to be searched for all sequence paths. For this, we can build a reduced control flow graph, which only contains the event publishing statements. Occurring function calls can be replaced with the control flow of the called function. As long as no recursion is used, the graph will be finite.
In the reduced control flow graph every event publishing is an action and the possible successor actions as well as end actions are known. For actions with static channels, we can then build the complete transition guard. However, for actions with variable publishing information we can only build an action template at compile time. If no further input is given by the system designer, we require runtime information to generate the action instances.
After model assembly we can use it to further our system understanding. This can be done with diferent verification methods at diferent stages in the software life cycle.
On the one hand we can run a static analysis during design time, before deployment. In this stage the system has no current state i.e. we do not know which components are connected. Instead, a reference state has to be defined for verification. This can be a default state or a scenario of interest. Since static analysis is not constrained by runtime requirements, it can be used with time or computation intensive verifications methods on dedicated hardware.
On the other hand, the model can be continuously updated for a dynamic analysis at runtime,
to verify properties on the current system state. Although, dynamic analysis can be resource
limited, it has the advantage of direct feedback. With our model we can reflect on the currently
executable behavior to inform about errors or trigger required system adaptations. This is
comparable to use cases envisioned in models@run.time by Blair et al. [
Additionally, not only the analysis phase influences the used verification methods, but also the unique system features. However, during modeling we collected properties that may indicate structural or semantic mistakes in the system design. Such properties can be defined once by experienced people and used anywhere in a general toolkit. Before we address custom business process specifications we like to give a short record of potentially general properties.
The model can be used with current Petri net model-checking tools for verification. During modeling we thought of this non-exhaustive list of properties that might be of interest to evaluate: • Live locks: Usually the system reacts to an input event with a finite sequence of followup events. Afterwards the system returns into a listening state where no transition can fire before a new environment event is introduced into the system. • Dead components: can this component be reached from an initial marking? • Distance: Given an event produced by a component, how many other components are needed before a token is produced on the event input of a target component? • Dead messages: is there an unproduced message type for an initial marking. • Short circuits: is there a component that can send messages to itself for any incoming message type? This behavior can cause a live lock and message flooding. • Event cascades: which events can be caused by a starting event (up to a maximum depth)?
If all possible cascades are finite the system will always "terminate" into a listing state. • Event sequences: can a sequence of events occur from a given initial marking? However, a graphical workflow specification can make verification more accessible, since it is more comprehensive. But to use workflows, a mapping to the system model is needed. 5.1.1. Business Process Mapping For the comparison of the publish-subscribe model with a business process, we first need a mapping relation between both. We assume the business process has the form of a WF-net and will address them as workflow from here on.
Finding a mapping is potentially the largest added human labor in our approach. Each task in the workflow needs to be mapped to a substructure in the implementation model. With a careful design the additional development overhead can be limited i.e. by mapping task names to matching event names. But this may not always be possible.
Every well-formed WF-net has three features that need to be mapped: a single start event a
single end event and the tasks that describe the business process.
Mapping the start event: Van der Aalst makes the case that workflows [
In contrast to a workflow in its end state, the execution of the publish-subscribe model can
continue. Usually other events exist and other component processes can be executed.
Mapping Tasks: The task semantics in a workflow is vague. Van der Aalst states that it
"corresponds to a generic piece of work" [
As a result an abstract workflow task transition may not map directly to a transition in
our model, because they represent dissimilar concepts. However, it is reasonable to assume
that a workflow task is constraint by a component process for the following reason: software
components in general encapsulate some functionality for system composition [
Yet, tasks and processes are not equivalent. Indeed, multiple tasks can be executed in a single process. In a special case, every task is represented by a single action. However, since actions are derived from code while tasks are derived from business processes, this perfect fit is unreliable. Actions with and without an associated task usually take turns.
Thus, some actions can be executed without an associated task and tasks may be associated with multiple actions. The latter case is divided into two variants: either the actions represent the same work just on diferent paths in the implementation (e.g. a call to publish in a function that is called at diferent locations), or the task spans multiple actions. If the task spans multiple actions it begins with an initial action and ends with a succeeding action in the current process. We know that the task is done, when the last successor action has fired. If multiple actions mark the end of a task because of conditions in the path, executing one is suficient to mark the end.
In an additional, undesirable relation there is no transition a task can be mapped to. This is the case for tasks that do not result in a significant state change in the publish-subscribe model. As a result no action transition is generated. Again, we assume this to be a rare case, because chances are, a system specification is reflected in the system implementation.
Nonetheless, this case needs to be resolved with a surrogate transition, marking task completion. A special surrogate is the execution of the end process transition: given a task is finished somewhere in a process, we know it is finished not later than the containing process. Alternatively, a dummy action, publishing a dummy event, added to the component implementation can be used as surrogate. Since a task completion is usually desired information, we can even consider this state change as significant and require a published event. Such events might also be desirable in other parts of the development, e.g. for logging. Otherwise, another existing action can act as surrogate if it is known to be executed after the task is done.
This leaves us with the following mapping possibilities: 1. Mapping the task to a single action. 2. Mapping the task to the last action(s) of a collection of connected actions. 3. Mapping the task to multiple actions that represent the same unit of work. 4. Mapping the task to a surrogate transition where the surrogate is one of the following: a) The Process End transition. b) A synthetic action added in the implementation, i.e.: publishing an additional event. c) A single or multiple actions on diferent paths, that are known to be executed directly after the given task has been finished.
The mapping relation then is a relation task → target where target ⊆ Action ∨ target ∈ Process.
With a workflow specification, the publish-subscribe model and a mapping relation between the two, we can collect assurance that the model conforms to the workflow.
Compared to the conformance checking literature [
A minimal conformance requirement is the existence of the previously discussed mapping. In a running system, components can connect and disconnect to the broker at any time. However, disconnected components cannot react to events making all internal actions unreachable. Since unreachable parts cannot be executed, we cannot map tasks of a business process to them. As a result a first inexpensive test can check the existence of a given mapping to all connected components. If no complete mapping exists, the workflow cannot be executed in our system.
If a mapping exists, further methods can be applied. Rule checking is a conformance checking
method that can be extended to our model. In rule checking, diferent rules are extracted from
the workflow to confirm the rules are observed in the event trace [
A more extensive, but also a more expensive, verification method can be based on a reachability
analysis. For both the workflow and the publish-subscribe model we can build a reachability
graph (given a finite state space). Having both graphs, we can check for similarity with diferent
approaches. Hens et al. suggested [
Without a pure equivalence we may show that all, or at least some possible workflow event sequences are observable in the publish-subscribe model. For this all transition sequences can be generated, and a model checking tool can verify the existence in the publish-subscribe net.
An even weaker equivalence can measure the alignment of transition sequences between
workflow and implementation model [
Additionally, van der Aalst describes workflow related properties that could be applied to our
model [
During runtime, our model changes e.g. if previously unknown components connect to the NoSe. As a result previously evaluated properties have to be reevaluated. Therefore, runtime evaluations need to be adjusted to the model complexity and the available resources. For example checking the existence of a mapping should be cheap while reachability based methods can get impractical. The methods of conformance checking seem like a good middle way between computability and expressiveness as well. And they have the added benefit to be directly applicable on observed logs besides event traces that where sampled from our model.
In this paper we presented a symmetric Petri net model of a publish-subscribe system for verification. We explicitly included a generic component model to represent the state of the composed system. Since the behavior of an EDA system is largely characterized by components interchanging events, our abstractions reduce events to types without event contents.
A framework conforming to our component model could use static code analysis to automatically compose a model instance from component implementations. However, the resulting model may depend on runtime information like involved components and channel names. In this case the model can be managed and adapted by the central notification service at runtime.
We showed which part of the model is static and which is dynamic. Since components are modelled explicitly, a mapping of business process tasks to model transitions can be found. This enables a comparison of the system capabilities, with business processes behavior specified as workflow nets. We showed a variety of methods that can be used for the comparison partially inspired by business process conformance checking. Some of these methods are inexpensive enough to be tested at runtime to increase assurance.
A framework implementation that supports building the model with a high level of automation is desirable future work. The minimally constraining component model still allows expressive process behavior but may also make model checking highly accessible for EDA systems.