Public and private server A system consisting of public and private servers. The system can generate an unlimited number of public servers and one private server. All servers are connected to each other. |
|
Public and private server 2 A modified version of the previous example. Adding of an error rule makes the abstraction refinement approach applicable. | |
Dining philosophers (finite-state version) A finite-state system of the dining philosophers: absence of deadlock states is checked by analyzing cycles in the hypergraph associated with the approximated unfolding. |
|
Dining philosophers (infinite-state version) The dining philosophers example as given above, but extended to an infinite-state system by adding a rule which allows an eating philosopher to reproduce. This rule creates another hungry philosopher with an adjacent fork. |
|
Firewall A network of secure and insecure locations, divided by a firewall. A simple distributed system with mobility, consisting of locations (secure and non-secure), processes running on these locations, and connections (secure, non-secure or firewall connections, which can only be crossed in one direction). |
|
Firewall 2 A modified version of the previous example. The property to be proven is that no process running on a non-secure location can influence a process running on a secure location, which can be formalized as the absence of causal dependencies between such processes. For this example the abstraction refinement should be used. |
|
Red-black trees Generate all possible red-black trees (a form of balanced search trees) and model the insertion of elements into red-black trees. |
|
Red-black trees converted A modified version of the previous example which can be analyzed more easily. Here we use Augur in order to show that the insertion of elements preserves the property that there are no consecutive red nodes in a tree, a requirement for red-black trees. |
|
External-internal processes A system consisting of public and private servers, internal and external processes. Public servers can extend the network by creating new connections; internal processes can wander around the network. The property to be proven here is that the external process is never connected to a private server and given access to classified data. |
|
Mutual exclusion A mutual exclusion protocol where a token is passed around. Only the process in possession of the token can use a shared resource. |
|
Resources A system of several processes sharing two resources. A process needs both resources in order to perform some task. |
|
Connections A simple attributed example describing an abstract dynamic system with changing attributes. There is also a special error rule. |
|
Leader election protocol A system modells a leader election protocol in a ring architecture with attributed graph transformation systems. The purpose of the protocol is to elect a unique leader from among the stations in a ring-shaped network. |
|
Needham-Schroeder protocol An attempt to model a well-known attack on the Needham-Schroeder protocol with attributed graph transformation systems. The purpose is to reproduce the attack in the obtained over-approximations. |
|
