Mcta

Benchmarks

The results on this page were obtained with Mcta's abstract distance function h^L which is based on the monotonicity abstraction. All results were computed on an Intel Xeon with 2.66 Ghz with Mcta-0.1. All benchmark files can be obtained in the download section. Dashes in the tables indicate out of memory (more than 4 GB). The results were obtained with the following command line options:

A* Search

f(s) = h(s) + depth(s), returns shortest error traces for admissible h

mcta -o3 -h5 -c2

Greedy Search

f(s) = h(s)

mcta -o2 -h5 -c2

Useless Transitions (UT)

f(s) = h(s) + depth(s) if s is reached via a useless transition, h(s) otherwise

mcta -o2 -h6 -c2

States with lower f values are preferred. If you are interested in more information about directed model checking, go here.

Single-tracked Line Segment

The Single-tracked Line Segment study stems from an industrial project partner of the UniForM-project [2] and the problem is to design a distributed real-time controller for a segment of tracks where trams share a piece of track. A distributed controller was modeled in terms of PLC-Automata [2, 3], an automata-like notation for real-time programs. The PLC-Automata were translated into timed automata with the tool Moby/RT [4]. For the evaluation of our approach we choose the property that never both directions are given permission to enter the shared segment simultaneously. This property is ensured by 3 PLC-Automata of the whole controller and we injected an error by manipulating a delay such that the asynchronous communication between these automata is faulty. In Moby/RT abstractions are offered for the translation into the timed automata. The given set of PLC-Automata had eight input variables and we constructed six models with decreasing size by abstracting more and more of these inputs.

		explored states			runtime in s			peak memory in MB			trace length
Exp.		A*	greedy	UT	A*	greedy	UT	A*	greedy	UT	A*	greedy	UT
C₁	.q	22501	1928	1658	0.3	0.1	0.2	60	58	58	54	100	91
C₂	.q	66791	4566	1333	0.7	0.2	0.2	65	58	58	54	132	91
C₃	.q	76777	6002	1153	0.9	0.2	0.2	66	59	58	54	128	91
C₄	.q	726516	81131	1001	7.0	1.4	0.2	130	70	58	55	344	121
C₅	.q	6.00e+6	430494	833	55.3	7.3	0.2	616	118	58	56	1057	114
C₆	.q	-	4.56e+6	833	-	63.9	0.3	-	632	59	-	3217	114
C₇	.q	-	-	829	-	-	0.4	-	-	59	-	-	114
C₈	.q	-	11.91e+6	816	-	144.3	0.3	-	1.4 G	59	-	5644	95
C₉	.q	-	27.74e+6	13423	-	326.8	3.2	-	3.0 G	73	-	5803	90

Mutual Exclusion

Mutual Exclusion is a case study that models a real-time protocol to ensure mutual exclusion of a state in a distributed system via asynchronous communication. The protocol is described in full detail in [3]. By increasing an upper time bound in the model we got a flawed specification that we transformed into its timed automata semantics by applying various abstractions techniques. The resulting models do not have many automata but a non-trivial amount of clocks and variables.

		explored states			runtime in s			peak memory in MB			trace length
Exp.		A*	greedy	UT	A*	greedy	UT	A*	greedy	UT	A*	greedy	UT
M₁	.q	34680	4581	4256	0.2	0.1	0.1	60	58	58	47	457	97
M₂	.q	135073	15832	8186	0.9	0.1	0.1	67	61	59	50	1124	146
M₃	.q	155164	7655	10650	1.0	0.1	0.1	67	59	60	50	748	91
M₄	.q	584221	71033	22412	4.5	0.5	0.2	96	70	66	53	3381	136
N₁	.q	80541	50869	5689	1.1	1.5	0.1	68	96	59	49	26053	108
N₂	.q	332486	30476	15377	5.6	0.4	0.3	92	70	63	52	1679	152
N₃	.q	406908	11576	16332	7.5	0.2	0.3	94	62	65	52	799	91
N₄	.q	1.59e+6	100336	44199	36.2	1.2	0.7	188	92	84	55	2455	118

Fischer

We use two variants of the Fischer protocol for mutual exclusion, which is well-known and scalable. The test examples are denoted FX_i in the tables, where X is A, B and i is the number of parallel automata. The error condition is that at least two of the i automata are in a certain location simultaneously. We made the error possible by weakening one of the temporal conditions in the automata (from "<" to "≤"). The variants differ in the way they encode the error condition (note that we have no disjunction in our language).

Variant A adds additional automata with synchronisation.

		explored states			runtime in s			peak memory in MB			trace length
Exp.		A*	greedy	UT	A*	greedy	UT	A*	greedy	UT	A*	greedy	UT
FA₅	.q	71	9	9	0.1	0.0	0.1	57	57	57	8	8	8
FA₁₀	.q	511	9	9	0.1	0.0	0.1	58	57	57	8	8	8
FA₁₅	.q	1701	9	9	0.1	0.0	0.1	66	57	57	8	8	8

Variant B selects and specifies two of the automata for the error condition.

		explored states			runtime in s			peak memory in MB			trace length
Exp.		A*	greedy	UT	A*	greedy	UT	A*	greedy	UT	A*	greedy	UT
FB₅	.q	54	179	7	0.0	0.0	0.0	57	57	57	6	12	6
FB₁₀	.q	429	86378	7	0.1	1.5	0.1	58	162	57	6	22	6
FB₁₅	.q	1504	-	7	0.1	-	0.1	67	-	57	6	-	6

Arbiter Tree

This case study models a mutual exclusion protocol based on a tree of binary arbiter processes. Client processes are situated at the leaves of the tree. In order to gain access to the shared resource, they may send a request to their respective parent, which in turn passes the request on to its parent, etc. When the root process of the tree receives a request, it generates a grant which is then propagated back down. When the client is done with the resource, it sends a release signal.

In order to avoid blocking client processes, arbiters need to be ready to receive requests from one of their children even when they are already processing one for the other child. In this case it makes sense to send a grant to the second child as soon as a release is received from the ﬁrst, instead of ﬁrst forwarding the release upwards and sending a new request. This can be applied asymmetrically (giving a grant to the left child ﬁrst, and always forwarding releases from the right child to the parent) in order to not monopolize the resource.

		explored states			runtime in s			peak memory in MB			trace length
Exp.		A*	greedy	UT	A*	greedy	UT	A*	greedy	UT	A*	greedy	UT
A₂	.q	73	36	15	0.1	0.1	0.1	52	57	57	12	21	12
A₃	.q	5168	206	32	0.2	0.1	0.1	59	58	58	17	24	17
A₄	.q	4.44e+6	76811	95	135.0	10.9	0.2	1.2 G	116	59	22	42	22
A₅	.q	-	263346	34	-	70.0	0.3	-	381	63	-	112	27
A₆	.q	-	-	39	-	-	1.0	-	-	80	-	-	32

Directed Model Checking for Real-time Systems