Modelling of Autosar Libraries for Large Scale Testing

TL;DR

This paper presents a model-based testing approach using QuickCheck for large-scale automotive software libraries, demonstrating precise specifications and automated testing for Autosar-compliant systems.

Contribution

It introduces a formal, state-full modeling method for testing Autosar libraries with QuickCheck, showcasing its application in industrial automotive software testing.

Findings

Successfully tested large parts of automotive libraries

Demonstrated precise, formal specifications for API and external interactions

Validated the effectiveness of model-based testing in automotive context

Abstract

We demonstrate a specific method and technology for model-based testing of large software projects with the QuickCheck tool using property-based specifications. Our specifications are very precise, state-full models of the software under test (SUT). In our approach we define (a) formal descriptions of valid function call sequences (public API), (b) postconditions that check the validity of each call, and (c) call-out specifications that define and validate external system interactions (SUT calling external API). The QuickCheck tool automatically generates and executes tests from these specifications. Commercially, this method and tool have been used to test large parts of the industrially developed automotive libraries based on the Autosar standard. In this paper, we exemplify our approach with a circular buffer specified by Autosar, to demonstrate the capabilities of the model-based testing method of QuickCheck. Our example is small compared to the commercial QuickCheck models, but faithfully addresses many of the same challenges.

Full text

1 Introduction

The multi-vendor and multi-platform character of automotive system development is a major challenge in testing the underlying software due to the multiplicity of possible software and hardware interactions and differences between various versions of the referenced libraries. Testing such software off-line brings the additional challenge of substituting low-level hardware interfaces and APIs with software mock-ups.

The Autosar standard [6] is an automotive industry effort to support multi-vendor software development. In particular, the standard specifies the basic software library interfaces and behaviour that Autosar compliant implementations should adhere to. Ideally, compliant Autosar components from different vendors should be interchangeable with little additional effort necessary to validate a complete system based on Autosar. However, in practice small differences in implementation choices due to performance considerations, particular platform limitations, or interpretation freedom for (purposely or inadvertently) underspecified behaviour may lead to compliance issues.

To manage the complexity of testing and validation in this context, we employ Model-Based Testing (MBT) techniques [12] rather than the classical unit testing approach. Because of the number of test cases necessary to cover the interactions and behavioural differences, unit testing suffers from scalability issues. In comparison, the base for MBT testing are models of the system and its components, based on which tests in an arbitrary quantity are generated on the fly. A carefully chosen test data generation method ensures a sufficient coverage (quality) of the resulting tests. New configurations and library versions of the system under test are simply covered by adapting the models and regenerating the tests for various configurations. Another important feature of MBT, as opposed to e.g. model checking, is that an actual running library or complete product compiled from a low-level language can be tested and validated, rather than its model (although in our particular case the model itself is also analysable, see Sect. 5). The infinite test space of this validation scenario obviously cannot be completely covered by MBT, however, the random test data generation ensures arguably good coverage of the code under test. The specification and the testing can be done with or without the source code availability for inspection, the latter being often the situation in our industrial projects.

Our MBT method of choice is property based testing using the QuickCheck tool developed by Quviq [3, 9]. In QuickCheck, a model is an Erlang [8] functional program that follows a predefined structure and API to form a behavioural description of a given software component. The properties that can be checked with generated tests are postconditions (test oracles) of single operations and call-out specifications. Call-out specifications are given in a process algebra-like language [11] and describe the calls to other components that the operation is allowed or required to make. The rest of the model defines the symbolic execution state of the component under test and operation preconditions, both of which define the valid execution traces for the tests to be generated. For the software under test written in C, which is the case for the Autosar components, QuickCheck provides a flexible interface that allows to abstract the C function calls in the model and run the underlying C implementation during the actual testing. The general philosophy of QuickCheck is to run several short tests quickly to detect problems early, rather than creating large and complex testing scenarios for which failures are extremely difficult to analyse. Should a larger test case need to be generated to exhibit a bug, QuickCheck offers a mechanism to shrink the test data to a smaller, possibly minimal, set that leads to the same failure. Consequently, the effort of debugging is also reduced.

QuickCheck has been used in large scale to specify and test Autosar basic software implementations [4]. In this paper we exemplify the QuickCheck method by presenting a small model for one of the Autosar components, a circular buffer for queuing arbitrary data. The client component is a message box system, that uses the circular buffer to specifically store message pointers (Sect. 2). Using this simple example we show how the multi-level component specifications are used to test Autosar implementations, and we show how C function mocking is employed in QuickCheck to test the call-out specifications (Sect. 3). Furthermore, we show how clustering specifications can be used to validate interactions between components within one functional set, i.e., that components respect each other APIs within a cluster (Sect. 3.4). The concrete implementation that we test comes from the open-source Autosar implementation by ArcCore111https://www.arccore.com., the third partner in the AUTO-CAAS project.

The mocking mechanism of QuickCheck for testing the call-out specifications is also used for checking the failure consequences in the complete system. This is done by mocking parts of the system with a behaviour specified by a model, into which we can incorporate known non-compliant behaviours or simply inject faults. This is described in Sect. 4. Then, Sect. 5 concludes the paper. The complete QuickCheck model for this case study can be found in App. A and on-line at http://ceres.hh.se/mediawiki/CirqBuff_and_MBox_QuickCheck_Models.

2 The Case Study

The case study we focus on is a circular buffer implementation CirqBuff [6]. The buffer has three core API functions, defined by the following C prototypes:

• •

CirqBufferType *CirqBuffDynCreate(size_t size, size_t dataSize); that creates a circular buffer of the given size which stores arbitrary data (byte sequences) of a given size;

• •

int CirqBuffPush(CirqBufferType *cPtr, void *dataPtr); that enqueues an element into the buffer, the element is passed through a pointer to the array containing the data to be enqueued. The result is 0 on success, otherwise 1; and

• •

int CirqBuffPop(CirqBufferType *cPtr, void *dataPtr); that dequeues an elementfrom the buffer by placing it in an array, and indicating the operation status with the return value.

The CirqBufferType is a C structure that keeps track of the current queue contents through the current element count currCnt and head/tail pointers to the allocated queue storage buffer bufStart …bufEnd, as well as the the static limits of the buffer – maximum size maxCnt, and the dataSize field, see Fig. 1 for the complete C structure definition. The data is copied to and from the buffer using one of the memcpy routines available on the target platform, this is one of the configuration options of this component that Autosar has multiplicity of, and that in general complicate the testing effort.

This circular buffer is used in a few places in the open source Autosar implementation, e.g., for communication transmission buffers. For presentation, we picked the simplest code available, a message box component that uses the circular buffer to store message pointers. The Mbox API is the following:

⬇

Arc_MBoxType* Arc_MBoxCreate(size_t size);

sint32 Arc_MBoxPost(**const** Arc_MBoxType *mPtr, **void** *msg);

sint32 Arc_MBoxFetch(**const** Arc_MBoxType *mPtr, **void** *msg);

The only field of the Arc_MBoxType structure is cirqPtr that keeps the circular buffer reference. The post and fetch functions are each a simple delegation of calls to CirqBufferPush and CirqBufferPop, respectively, with the same meaning of result values. Arc_MBoxCreate creates a circular buffer with the data size fixed to the pointer size sizeof(void *). Thus, MBox specialises CirqBuff to store pointers.

3 Specifying and Testing the Implementations with QuickCheck

Tens of software components for vehicle software are specified in Autosar in a modular way. The task at hand is to modularly test both CirqBuff (Sect. 3.1) and Mbox (Sect. 3.3) implementations. However, we also want to test the software together, i.e., the component integration. We do so by automatically deriving its specification (Sect. 3.4).

Using MBT, one first builds a model, the specified behaviour of the software under test (SUT). Based on the model, an arbitrary number of test cases can be generated. Test cases are sequences of calls to the API functions with generated data parameters. In addition, the test contains information of what external API calls the SUT makes. These API calls are automatically mocked. The generated tests are then executed on the SUT and the tool validates postconditions and call-out behaviour for each call.

As MBT tool we use Quviq’s QuickCheck with two distinguishing features: expressive, state-full, executable models, and failed test minimisation, called shrinking. Shrinking is a mechanism for reducing the size of the test case that failed, so that it still leads to the failure, but with a possibly (much) shorter execution trace. The controllable (see Sect. 4) data generators make this possible.

3.1 The CirqBuff Model

A snapshot of the QuickCheck model for CirqBuff for discussing is shown in Fig. 2, the complete model is quoted in App. A. The model is a collection of Erlang [8] functions describing the different aspects of the behaviour of the component under test. First, the declared record type cb_state holds the symbolic execution state of the model, i.e., a model view of the CirqBuff’s current state. It contains the pointer ptr reference of the freshly created buffer by the CirqBuffDynCreate, the size and the data_size requested during the creation, and the model contents of the buffer elements, an Erlang list of arbitrary values. The state is initialised by initial_state which defines elements to be an empty list representing an empty buffer. The remaining fields of cb_state are set to undefined.

The invariant function declares a condition to be checked throughout the execution of the actual tests. Here it is defined somewhat artificially, because its validity is guaranteed by the construction of the rest of the model (it only refers to the model state, not the implementation state), but in general it can be used to check specific validity conditions of the implementation, e.g., the head pointer to be within the bounds of the CirqBuff storage buffer. Similarly, the common postcondition is checked after every CirqBuff operation call during the actual test. Using Erlang parameter matching, we state that no extra checks are necessary for the create call, the postcondition is true, while all the other calls should have their actual return values equal to the ones specified by the model. These model return values are specified separately for each operation, as we describe next.

For every API operation we declare a group of callback functions that define:

How to call the C function to execute the actual test (the base callback); 2. 2.

How to generate its arguments (the _arg callback); 3. 3.

What is the precondition, defined over the model state and operation arguments, for the operation to be eligible for execution (the _pre callback); 4. 4.

What is its expected return value (the _return callback), and finally; 5. 5.

How to update the model state after the operation is executed (the _next callback).

Each operation can have its own specific postcondition defined with a _post callback and a call-out callback to specify internal and external API interactions, we describe this in the next section. The obligatory callbacks are the base one and the arguments one, through which QuickCheck recognises that an operation should be part of test generation. The others have default values if unspecified.

The create arguments are two positive integers indicating the queue size and data size. The queue size is restricted to be strictly positive by the precondition of create. Thus, all data sets generated that have the size equal to 0 are rejected during test generation process. The precondition also requires that create is called only once per test when the queue is not yet initialised, i.e., when no queue pointer reference has been recorded in the model state. The new model state after create is one with the newly created pointer and the creation arguments recorded in the corresponding fields of the state record.

The first argument of the push operation is the pointer stored earlier in the model state. The second argument is an element to be enqueued, here a random data_size length sequence of characters. The precondition limits the push calls to initialised and not yet full queues. Due to this precondition, the expected return value is 0. In the next state the newly enqueued element is recorded in the elements list. The pop operation is a mirror of push with no new specification concepts, hence we skip it in Fig. 2.

The precondition, arguments, and the next-state callbacks are primarily used during test case generation, i.e., when the model is symbolically executed to generate valid execution traces with sample input data. The base and the return value callbacks, together with the postcondition and the invariant described above, are used during the test execution to

(a) trigger the actual C implementation call, and

(b) check the correctness of the result.

The model state is updated both during the test generation, and test execution for bookkeeping. In the former case we refer to it as symbolic state, in the latter as dynamic state.

The execution of create involves a direct call to its C implementation CirqBufDynCreate with the generated arguments. This wrapped C call is automatically generated by the QuickCheck C interface generation library eqc_c. A particular instance is set up by calling:

⬇

eqc_c:start(cb, [ {cppflags, "-std=c99"}, {c_src, "cirq_buffer.c"} ]).

However, the CirqBuffPush C implementation expects the data to be passed through a pointer, and this pointer has to be created first from the pure data generated by QuickCheck. This is done with the QuickCheck library function eqc_c:create_array that delegates pointer creation to the C executable, which is then passed on to CirqBuffPush, after which it can be immediately freed, see again the specification of push in Fig. 2.

3.2 Testing CirqBuff with QuickCheck

The model-based test execution of a specified component in QuickCheck is done through defining a test property and passing it on to QuickCheck, see Fig. 3. A test sequence is generated with commands for the model specified in module qc_cb. The generated test sequence is executed with run_commands(Cmds). The repetitive generation of test cases is controlled with the ?FORALL construct, by default 100 random tests are generated. Additional parameters can be used in the property and the model, e.g., to induce the creation of more or longer test cases or to collect specific test statistic (e.g., requirement coverage [2]). In the simplest form we just state Res == ok to check for the result of running each test. Passing this property to QuickCheck results in passing all 100 tests.

In fact, we can run thousands of tests that exercise the creation of circular buffers with different sizes and data sizes. We push and pop from these buffers without finding any error in the implementation. Notably, with the specific model construction we do respect the interface and never try to overflow or underflow the buffer.

3.3 The MBox Model

By essentially copying and pasting the specification, we could test MBox in exactly the same way. However, being a client implementation that uses CirqBuff as a library we want to take a different approach that details this dependency. We test MBox in isolation and use mocking for the CirqBuff calls.

The general idea of mocking is to execute a test of an upper level operation (here from Mbox) in an environment, where the lower level operations (here from CirqBuff) are replaced by emulated (mocked) ones. This enables tracing of the particular low-level calls actually made (or omitted, in case something should be forbidden), and to check the call arguments. It also facilitates testing of software that uses hardware interfaces that cannot be run outside of the target platform (e.g., ECU ports or A/D converters).

Code mocking is generally a tedious task involving writing replacement code of the mocked functions. QuickCheck has an interface that makes the process considerably easier and provides a flexible language with clearly defined semantics to specify the interactions with the mocked component [11]. Mocking of a component is enabled by providing its API description in the model, such definition for CirqBufPush is given in Fig. 4. With just the API, QuickCheck replaces the CirqBuff implementation with an emulated alternative. The stored_type and buffer clauses indicate that the dataPtr parameter should not be simplified from a pointer to just a value during mocking (which is the default behaviour), and because void has no values, the type is changed to unsigned char to enable dereferencing values from pointers.

The specification of MBox follows the same pattern as in CirqBuff, here we only underline the core differentiating elements. The message enqueueing operation post is specialised to store pointers, i.e., byte sequences of ?PTR_SIZE length exactly, thus data size is not stored in the model state. The _callouts callback specifies the external calls of post. Here, a single call to CirqBufPush is required with two arguments. The first is the pointer to the CirqBuffType structure that is created by MBox earlier with a call to CirqBuff’s create function. We choose to ignore it with ?WILDCARD, meaning that we do not check if MBox uses this pointer consistently with all CirqBuff calls. The second argument is the value pushed onto the circular buffer and it is simply passed on from the call to post. The result of the call should always be 0 indicating a success.

Specified this way, MBox can be tested with the CirqBuff fully mocked and with all the calls to CirqBuff traced and checked. The MBox test property is identical to the one for CirqBuff, the difference in test generation and execution lies in the mocked API specified in the model. Should the calls to CirqBuff made by MBox be different from the specified ones, or missing, the test fails and the details of the mismatch between the expected and actual calls is reported.

3.4 Analysing Models and API Interactions through Clustering

We have specified only two components, one depending on the other, and we have shown how the interactions down this simple hierarchy can be modelled and tested through mocking and call-out specifications. This scenario, however, is very simple. Moreover, we only tested for the occurrence of the lower-level call in relation to the state of the higher-level model and the particular operation parameters. More generally, we would like to test multi-level dependencies of several components and check that they all fully respect each other APIs according to the corresponding model specifications. For example, so far we did not checked that the MBox is not trying to overflow the circular buffer by placing too many elements in it.222Actually, incidentally it was checked implicitly, but only because of the specific model construction and the fact that the sizes of the two components are always the same. It was not done explicitly by checking the preconditions of the circular buffer. A typical example of a scenario requiring such elaborate check is a protocol stack, in Autosar there are several such protocols specific to automotive applications, including CAN-Bus and Flex-Ray.

To enable such a check, the set of interacting components is placed in a so-called cluster model. The models of components placed in a cluster only need slight extensions to facilitate the process. First, the operations that can be called by other components have to name the possible callers by their module name. Second, the API specifications of the mocked calls to the lower-level routines need to have a direct indication specified as to which modelled component and operation in the cluster they refer to.

In our case study, each operation in the model of the CirqBuff has to name the MBox model as the caller of the operation. For the push operation this is done with push_callers() -> [qc_mbox]. Then, the mocked API for CirqBuffPush is extended with a classify = {qc_cb, push} clause to indicate the binding to the appropriate operation in the CirqBuff model. These two simple extensions repeated for every operation allow us to now give a short and straightforward cluster specification for the two components shown in Fig 5. It simply lists the components in the cluster and defines their underlying collective API by collecting the APIs of all included components. Testing the specified cluster property by QuickCheck establishes that MBox respects the API of CirqBuff. Namely, if any of the MBox calls is eligible to be included in the generated test case for MBox, then the corresponding call-out to CirqBuff is checked to be eligible in the CirqBuff model. This includes checking that the caller is an authorised one. This is done by pure symbolic execution of both models, no actual implementations are tested in this process, it is only the models and their interactions that are checked. The actual implementations are tested one by one using their corresponding models like described above.

4 Faults, Deviations, and Consequence Testing

The mocking mechanism discussed in Sect. 3.3 also allows us to test implementation against mutations of sub-components to test for fault tolerance. This is part of on-going research [5, 10], here we exemplify the idea and show the capabilities of QuickCheck to guide test generation to trigger a hidden fault.

Assume a scenario where the CirqBuff has either faults, or deliberate modifications dictated by, e.g., performance optimisations or target platform limitations. These changes may or may not be compliant to the specification given by the standard. When they are not we call them deviations, rather than just faults. Done in good faith, they do not necessarily have to lead to problems or faults in the top-level behaviour. We want to model and test for this, without going through the burden of modifying the implementation of the low-level component, or constructing several implementations for this purpose. Instead, we test using the mocked version of the possibly deviating component and introduce the deviation in the mocking.

Suppose the CirqBuff silently accepts all buffer sizes when creation is requested, however, due to platform limitations only buffers of size 128 are created, under the assumption that the client code can check the available space each time a new elements is enqueued (which in fact our particular client MBox does not do). To include this behaviour in our model it is sufficient to make one line change in the call-out specification of CirqBuffPush to return 1 on reaching the “silent” limit of 128 elements:

⬇

?CALLOUT(mbox, ’CirqBuffPush’, [?WILDCARD, Value],

    **if** **length**(S**#mbox_state**.elements) < 128 -> 0; **true** -> 1 **end**)

Regenerating the tests with this updated model does not reveal any problems in the implementation of MBox, while it should. The reason is the nat() size generator that does not attempt to create MBox-es of sizes large enough, and even if it would, the generated traces do not contain enough post operations to fill up the buffer and trigger the fault. To stimulate QuickCheck towards reaching the faulty state we first change the size data generator from nat() to choose(1, 256) that uniformly generates integers in the prescribed range rather than conservatively small ones. Then, we alter the test property with more_commands to increase the expected length of generated test traces by the factor of 50, and we provide relative weights to ensure that the post operation dominates in the generated tests to quickly fill up the buffer, see Fig. 6. This is sufficient to discover the fault after a handful of test runs by QuickCheck. Expectedly, the shrinking algorithm is not able to generate test cases shorter than 130 commands to trigger this fault, however, 130 is the minimal fault triggering trace – one create, 128 post-s to fill up the buffer, and one last to overflow it.

Similarly to more_commands, with the more_bugs directive QuickCheck attempts to discover more than one fault in one testing sessions, instead of halting after the first test failure. This way, different kinds of faults (different postconditions failing) can be identified sooner.

An often quoted criticism towards MBT is the high specification to implementation ratio, here roughly 1:1 which is equivalent to a reimplementation effort. However, this is all the effort required – with one or two line changes to the model we have just shown how to test the implementation against a different sub-component and how to substantially change the shape of the generated test cases to trigger a hidden fault. In the classical testing approach, a large number of new test cases would have to be developed as well as complete component implementations to achieve the same effect.

Finally, some remarks about the test execution and bug finding time performance should be made. The complete process of generating the basic 100 test cases for the MBox implementation in its initial configuration from Sect. 3.3 (i.e., with CirqBuff mocking, but without custom operation weights and without more_commands) and executing them takes a mere 3 seconds on a standard laptop. Expanding the test scenario to hit the bug increases this time to 36 seconds, which is also acceptable. Moreover, this is the time for generating and executing all 100 tests, but the bug is found after just $\sim$20 tests in 7 seconds. Specific test scenarios that attempt to find an infrequently occurring bug may require increasing the standard 100 random tests towards a much larger number (tens or hundreds of thousands). However, the running time will grow only linearly to the number of tests, which is perfectly acceptable considering the goal of finding the bug and the full process automation.

What does take considerable time is the shrinking process for large counterexamples. In the example we have shown in Fig. 6 it already took just under 6 minutes for the counterexample trace of 218 operations. This is because each single shrinking attempt requires at least one complete rerun of one test case to check if the bug still occurs with the smaller trace. This procedure, however, is again fully automatic and replaces laborious, time consuming, manual process of analysing and rearranging test cases by the test engineer to find a shorter counterexample.

5 Conclusions

Using a small example from the automotive Autosar standard we have presented the QuickCheck methodology for model-based testing. By generating tests from models, instead of manually writing them, we can cover an arbitrary set of test scenarios. By controlling test data generators, we can drive the process towards a specific testing goal. The randomness of test generation brings the additional advantage of creating a-typical test sequences that would not be considered by a testing engineer.

The added value of model-based testing is that we can arbitrarily raise the number of tests to cover new behaviours of the system under test with very little additional effort. In our small case study, changing a couple of lines in the model exhibited a hidden bug, while the shrinking mechanism of QuickCheck provided a minimal counter example for the bug without extra development cost, in favour of additional running time to crunch the test data.

An indispensable feature of QuickCheck is the flexible API mocking mechanism. Apart from enabling software abstractions of hardware interfaces, which is crucial for off-line testing of embedded software, we have demonstrated how it can be used to test for fault tolerance of the complete system. We achieved this by injecting faults in the component mock-ups, against which the system is tested. This allows to test against many different (faulty or correct) component implementations, that in fact do not have to and may not even exist, provided a configurable model of the component is available.

Similar to writing test cases, building the models requires domain knowledge and the ability to interpret the specifications written in English. But by domain experts, it is conceived harder to write a model than to write a single test case. This is not QuickCheck specific, but a general observation that reasoning about all cases at once is harder than reasoning about one specific case. When the hurdle of writing models is overcome, a second challenge, a technical one, is to learn the modelling language. It takes a course and some weeks of experience before engineers feel comfortable with modelling C code in Erlang.

In the presented case study that mimics the real testing effort of the Autosar software, the specification to implementation ratio is 1:1. However, as the code grows towards the complete Autosar library, the size of the model does not grow as fast. For the complete set of Autosar libraries that has been tested commercially [4] the models are only about 20-25% the size of the feature rich C source code under test. Obviously, specifying real Autosar libraries on a larger scale brings additional challenges and benefits compared to what we have described in the paper.

On the benefits side, we can create test suites for really complex library configurations using the same models. This is not so obvious in our example, but an Autosar configuration file consists of thousands of parameters. Inspecting and updating manually written test cases for such a parameter space is really hard. When using models, we can do this automatically.

Another benefit that is hard to see in the paper, but showed valuable in production is the clustering. A typical test case for the CAN bus would cover five different specifications, from driver up to CAN State Manager (CanSM) and CAN Interface (CanIf) [7]. Each such specification is a separate document. There is no detailed specification on how the complete stack should behave. Therefore, engineers manually constructing those tests must have all possible interactions in their head. And indeed, this is error prone. We encoded the six test cases provided in [7] in our format, and executed them against the model. We found that three of the six tests agreed with our model (i.e., these tests would possibly be generated by our model); the other three were not accepted by it. So we could never have generated these tests – but this turned out to be a good thing: the three standardised test cases failed to consider a specific transmission recovery scenario. This has been acknowledged as an error, and is filed in Autosar’s Bugzilla for correction in the next release. In other words, being able to compute the complex interactions instead of trying to imagine them, is an advantage.

On the challenges side when dealing with larger models is to get those models generate valid test cases. There we used implementations from different vendors to validate against and to discuss cases in which our models and C implementation did not agree. In this process, ambiguities or underspecifications were found in the standard that lead to differently behaving stacks, whereas they were all arguably correct. This is a strength and weakness of low-level modelling; on the one hand one wants to make all differences on the API level visible, on the other hand, some design decisions that make an implementation faster or less memory intensive, may be tolerated. The QuickCheck methodology had problems in tolerating “that is also fine” approach.

Another effort not visible in small, simple examples is finding good values for test distribution. In the larger models we needed to add certain distributions to get into some interesting states more often. For example, if a large message is sent in chunks over the CAN bus, one wants at least one test that finishes the complete transfer. If the API calls are chosen just at random, this is unlikely to happen. Therefore, such behaviour needs to be guided by test distribution values.

Appendix A The Complete CirqBuff and MBox QuickCheck Model in Erlang

Below we present the complete model discussed in this paper. The snippets used for presentation are slightly abbreviated and simplified for clarity, here the specifications are given in their full form, also to be found at http://ceres.hh.se/mediawiki/CirqBuff_and_MBox_QuickCheck_Models.

A.1 File sourcepath.hrl

A.2 File qccb.hrl

A.3 File qccbsetup.erl

A.4 File qccb.erl

A.5 File qcmbox.hrl

A.6 File qcmboxcapi.erl

A.7 File qcmboxsetup.erl

A.8 File qcmbox.erl

A.9 File qccluster.erl