Programmable Messaging for Electronic Government - Building a Foundation - Formal Methods and Hybrid Real-Time Systems - page 221

Fig. 1. Licensing food and beverage establishments - business process

4.1 State

The data model described here is the basis for expressing messaging behaviours
in subsequent sections. Essentially, the model defines the notion of a state - a set
of variables belonging to different members, and behavior models capture state
changes caused by sending and receipt of messages. Variables and messages have
the same internal structure - a set of parts of different categories, and a linear
ordering on the parts of the same category. A type hierarchy is also defined to
determine which parts are optional and which are mandatory inside a variable or
a message, with subtyping relation defined between pairs of types. The top-level
type requires all structures to contain three mandatory parts: an identifier to
uniquely represent a structure, a type to determine the required composition of
a structure, and a member to represent the owner of a variable or the sender
of a message. Every part has a category and a value, with pairs of symmetric
functions provided for each category to construct and deconstruct part values.