Towards the Property-Based Testing of an L4 Microkernel API Cosmin Dragomir Lucian Mogosanu Faculty of Automatic Control and Computers Faculty of Automatic Control and Computers University POLITEHNICA of Bucharest University POLITEHNICA of Bucharest Splaiul Independentei nr. 313 Splaiul Independentei nr. 313 Sector 6, Bucuresti, Romania Sector 6, Bucuresti, Romania cosmin.dragomir@cti.pub.ro lucian.mogosanu@cs.pub.ro Mihai Carabas Razvan Deaconescu Faculty of Automatic Control and Computers Faculty of Automatic Control and Computers University POLITEHNICA of Bucharest University POLITEHNICA of Bucharest Splaiul Independentei nr. 313 Splaiul Independentei nr. 313 Sector 6, Bucuresti, Romania Sector 6, Bucuresti, Romania mihai.carabas@cs.pub.ro razvan.deaconescu@cs.pub.ro Nicolae Tapus Faculty of Automatic Control and Computers University POLITEHNICA of Bucharest Splaiul Independentei nr. 313 Sector 6, Bucuresti, Romania nicolae.tapus@cs.pub.ro Software testing has been a significant part of the software development process for the last 30 years and is gaining even more importance with the increasing complexity of software products. As each application has its own requirements, multiple software testing methodologies exist. It is the decision of the developers to choose the best suited types of testing methodologies for their product. This paper presents the design and implementation of a property-based testing framework. Unlike traditional testing methods this methodology uses the formal specification of the API to automatically generate the input and validate the output. The framework will be used to test the API of an L4 microkernel (called VMXL4); VMXL4 possesses the constraints of an embedded environment and of an ongoing development of a stateful system. Property-Based Testing, L4 Microkernel, API 1. INTRODUCTION specification”, in which tests are written to cover most of the specification. The software industry has been constantly growing in the last decades and the liability and robustness of Writing a large number of tests for the same the software products must match their requirements specification implies a sizable effort from the in order to remain competitive. To obtain a stable developers. Property-based testing mitigates this product, the entire software stack must be reliable. by automaticallly generating the input and creating Therefore software testing must be done at each general and abstract tests known as properties. layer of the software stack, starting with the lowest Those can be similar to unit tests, except for the way level: the operating system. input is generated and output is validated. Multiple software testing methodologies are in use This paper presents an user space framework nowadays, each of them targeting a degree of named QC that is based on an open source basic im- test cases coverage and test writing complexity. plementation of a property-based testing framework Alongside the well known unit testing method, implemented by Pennebaker (2012). Although the another functional methodology named property- well-known related released frameworks are written based testing has gained ground among software in functional programming languages, QC is written developers. It uses the concept of “tests as in C due to the VMXL4 native environment support.  • • • • Porting a new language environment would have At a higher level, software testing can be defined meant a sizable and unnecessary effort. as the process of executing a part or the entire application in order to find errors or to evaluate the The QC framework solves issues commonly encoun- quality of the user experience. Any moderately sized tered in unit testing by using properties and testing application has flaws, but finding them is a complex those properties on a large number of randomly activity. It is usually unfeasible to do an exhaustive generated inputs and by maintaining the internal testing on stateful systems, since the number of state of the system. As a downside, QC introduces different possibilities for the input values associated the problem of formalizing the specification. with the existing internal system state is too large. Even for some stateless applications this testing The paper is organised as follows: Section 2 is would imply a sizable effort. We conclude that it is introducing the concepts necessary to understand more resource and time demanding to test a stateful the paper. Section 3 briefly presents the existing system instead of a stateless system. similar frameworks. Section 4 discusses the design and implementation of QC and Section 5 its There are multiple methodologies in software testing evaluation in comparison with the existing testing which must be used in various steps of the methods for the API of an L4 microkernel, VMXL4. development process. In this paper we insist only Lastly, in Section 6 we present the overview of the on those that can be split in two major categories: paper and future work. functional and nonfunctional testing. Functional testing verifies the client or design 2. BACKGROUND specifications by testing the system functionality: This section presents the basic concepts required checking if the program operations and features to understand the next sections of the paper. It behave as they should. In summary it is used to starts with the overview and importance of software ensure that the application does not have bugs. testing, followed by the essential concepts of unit There are two categories of functional testing: testing and property-based testing. We show the positive and negative. Positive testing is done using power of property-based testing in contrast with unit valid inputs and comparing the actual output with the testing. We also do a short introduction of the testing expected output, whereas negative testing is done environment, describing the VMXL4 microkernel. by supplying the system functionalities with invalid or unexpected inputs and operations. In the case of 2.1. Software Testing negative functional testing, usually the system must not behave nondeterministically and rather inform Nowadays the number of different programming lan- the user of the input error. guages, hardware platforms and software libraries is increasing. Requirements, for both specifications On the other side, nonfunctional testing is concerned and performance, are also more rigorous as time with the user experience, including tests for passes by. As a consequence, software applications performance, security, availability, usability. Using are becoming more complex and bugs are intro- this type of testing, one can measure and compare duced in new software at all levels. As a countermea- the results in different situations and cover the blanks sure software testing has gained more importance left by functional testing. For a competitive software and attention from programmers. product, developers must test the program using both functional and nonfunctional methodologies. It is important that applications and services can be stateful or stateless. In a stateful system, an internal 2.2. Unit Testing state is being held and some of the actions have side effects which might change the state. The design of One of the most used and successful software a stateful software system can be modeled using testing methodologies is unit testing (Binder (2000); a finite-state machine and a formal specification of Hunt et al. (2004); Osherove (2010)). It is centered the inputs for every possible state. The summarizing on the concept of unit of work, meaning a single, difference between stateful and stateless systems invokable, logical and functional use case of the is that for the first one the output depends on the system. input and possibly on the internal state, whereas for Unit testing is composed of a suite of tests that the second one the output always depends only on can be run anytime during the development cycle to the input. A well known example of stateful versus test certain functions, logic and capabilities of the stateless are the TCP and UDP transport layer code. Each test uses a predefined set of inputs, protocols from the TCP/IP stack, where TCP creates runs a functionality of the system and compares and maintains a connection between the client and the output with the desired output. If the outputs the server and UDP does not. • • • • differ, the tested functionality has at least one bug. A generator is a callback that does random data Although unit tests usually verify only one small generation at each running of the property. Because feature, sometimes it is not easy to find the bug, complicated non-basic data types may be needed, a due to the black-box nature of the methodology. This property-based testing tool must allow user defined means that unit testing does not use the internal generators. In order to achieve a good test coverage, structure of the functionality, but only the higher level the generated data must be uniformly distributed invoked part, and therefore the bug may be in the across its domain. internal logic and further debugging must be done. One big advantage of unit testing is its reusable To show the differences between unit testing and nature. Even if the internal logic changes, usually the property-based testing, let’s assume one would want requirements of the function remains the same and to test a function named getMax, a function which the old test can still be used. returns the maximum of two integer values. In a unit test he would hard-code two values and test Although unit testing is very useful, it has a very if the output equals to the maximum value. If he important flaw, which may leave hard detectable wants to test multiple cases, possibly corner cases, bugs in the system. Using unit tests a programmer then multiple tests need to be written. A pseudocode only verifies a small finite set of inputs and for implementation of the unit test is shown in Listing 1. every different input set he must write another test. max = getMax ( 2 , 5 ) Therefore, using unit test programmers cannot even a s s e r t ( max == 5 ) get close to an exhaustive testing. In addition to not finding possible subtle bugs, the work of the Listing 1: Pseudocode for getMax unit testing programmer is hardened by thinking of all the corner cases and writing more code for them. In the end, Using property-based testing, a pseudocode imple- these drawbacks are less important than the benefits mentation would be the one from Listing 2. of unit testing: because it gives good results in practice, it is very used and every major language a = generator ( ) has frameworks for this testing methodology. b = generator ( ) max = getMax ( a , b ) 2.3. Property-Based Testing a s s e r t ( ( max == a | | max == b ) && ( max >= a && max >= b ) ) A software testing methodology which addresses Listing 2: Pseudocode for getMax property-based the problems left by unit testing is property-based testing testing (Fink and Bishop (1997); Fernandez et al. (2004); Machado et al. (2007)). Its main advantage is that it covers substantially more test cases than As shown above, the property is generic and more unit testing; moreover, it can do exhaustive testing powerful than the unit test. However, the validation though the time required to do this is not directly condition is bigger and must be correctly determined proportional to the benefits. This is done using by the test writer, otherwise the property may give only one generic test, named property, and some false positives or, even worse, false acceptances. functions to generate the inputs, named generators. The quality of the automatic testing tool may be A property is the replacement of a unit test improved by reducing the number of failing test and is run multiple times with different automated case inputs in order to obtain the minimum set of generated inputs. Every running of the property inputs determining a given failure, a method known generates a different test. The input of the property as shrinking. This has the advantage of improving depends on the type and domain specified by the debugging process by providing the programmer the programmer; because the input is generic, with minimal necessary information for debugging; the validation conditions of the test must be also another advantage is that the overhead of this generic, following a formal specification. The name method is not significant. “property” comes from the type of test validation, where each test result must pass a general formal All in all, property-based testing has the benefits of property. In layman’s terms a property validation unit testing and some advantages over it: bigger test condition specifies in a generic way how the tested coverage, improved specification completeness and functionality should behave. A drawback of property- it is easier to maintain because of the reduced code based testing is that the formal specification does not size, as illustrated by Nilsson (2014). usually exist and the programmer must infer it from 2.4. VMXL4 the business and logic specifications. VMXL4 is a general purpose, high performance L4 microkernel (Liedtke (1995)), developed in We propose that the QC testing framework presented in Section 4 use the same testing design, with the addendum that additional support libraries may be needed, e.g. in order to generate random numbers. This converges with our goal to provide a POSIX compliant native environment based on VMXL4. 3. FRAMEWORKS FOR PROPERTY-BASED Figure 1: VMXL4 testing infrastructure TESTING The idea of a property-based testing framework is 1 partnership with VirtualMetrix, Inc . It provides not new. Previous frameworks have been developed, mechanisms for performance management and a but the most successful are for functional languages, minimal layer of hardware abstraction on which due to some of their distinctive features: higher order virtualized operating systems personalities can be programming, which is very useful for properties built. Using the VMXL4 API, trust and security and data generators, lack of side effects, time of models can be implemented. Examples of systems development. Moreover, functional programming fits built using VMXL4 are given in Carabas et al. (2014), better for random testing than imperative program- Manea et al. (2015) and Mogosanu et al. (2015). ming because it uses fine-grained properties. This section presents an overview of three of the most An L4 microkernel was chosen due to the fact that influential existing frameworks and of some open the L4 API’s formalization was proven to be feasible source projects. by Kolanski and Klein (2006). The seL4 microkernel is the first operating system kernel to be fully formally Haskell QuickCheck specified and verified, as shown by Elkaduwe et al. Haskell QuickCheck2 is the first well known (2008) and Klein et al. (2009). Furthermore, other framework for property-based testing and future implementations have been proposed for formally frameworks were inspired by it. QuickCheck is a verifiable L4 microkernels (Kauer and Völp (2005)). tool which automates testing for Haskell programs. The property-based testing approach proposed by As shown in Claessen and Hughes (2002, 2011), it this paper is in some respects similar to previous does this by defining a formal specification language, work, as it also relies on a formal specification. which is powerful enough to represent common The most important difference between the two forms of specifications: algebraic, model-based and approaches is that property-based testing is more preconditional or postconditional. QuickCheck uses efficient in terms of development resources, as combinators to define properties and test data opposed a full mathematical refinement proof, which generators and obtain the test generated data may require a significant number of man-months to distribution. An important feature of the framework be implemented. is the shrinking of the generated data when a test fails, to give the minimum input which still fails the Figure 1 shows the architecture of the current property. VMXL4 testing infrastructure. The L4 microkernel runs in the privileged CPU mode commonly known Erlang QuickCheck as kernel space, while the tests run as user The programmers who developed Haskell space applications. The testing infrastructure is QuickCheck saw the bigger commercial opportunity implemented using support libraries, but the test offered by Erlang and developed a new version themselves call the L4 API directly in order to of the framework3 , which has its specifications in validate it functionally. Erlang. Linking specification in Erlang to code under test in other languages is easier than in Haskell. Currently most API tests are following unit testing Two very important distinctive features of the Erlang principles, so test coverage is not nearly as exten- version are the ability to test stateful systems sive. However, microkernels are stateful systems, by using state machine testing and the ability to some of their core mechanisms being strongly cou- generate and run parallel test cases in order to find pled. As a result, the current testing framework does race conditions (Arts and Hughes (2003)). not employ true unit tests and only partially validates 2 https://hackage.haskell.org/package/QuickCheck the interaction between components. 3 http://www.quviq.com/products/erlang-quickcheck/ 1 http://www.virtualmetrix.com/ • • • • ScalaCheck 4.2. General Design ScalaCheck4 is the third main framework used for property-based testing and is used for automated Because a kernel is a stateful system and QC is randomized property-based testing of programs developed to test the L4 microkernel API, being developed in Scala or Java (Odersky (2010)). It evaluated on VMXL4, two more concepts used by was inspired by Haskell QuickCheck and implements QC have to be introduced. Preconditions are a set of most of its features, but also some in addition to its predicates that must be true prior to the execution of predecessor, such as stateful testing. Nilsson (2014) a property and postconditions are a set of predicates provides a comprehensive guide to ScalaCheck. that must be true after the execution of an action in the property. If all the preconditions of a property are Open Source Initiatives true, then the property is applicable, otherwise it is Due to the success of Haskell QuickCheck, open not. If all the postconditions of a property are true, source implementations in most major programming than the property has passed. languages were started, such as C, C++, Java, Python, but with less features and success. QC was Due to the fact that QC is designed for a stateful inspired by one of those open source initiatives, system, it uses tests containing multiple properties employed by Pennebaker (2012). that are used as actions with side effects in the stateful system. Therefore QC borrows some elements from integration testing, a methodology 4. QC DESIGN AND IMPLEMENTATION in which individual software modules are tested together. Each test consists of at least one property, This section presents the design and implementation randomly generated from the available properties. of the QC framework and the motivation behind Each property has a finite number of arguments it. QC intends to test the L4 microkernel API in with known data types at compile time, a fact a functional manner, following the property-based that provides the opportunity to use property-based testing methodology. It may be used alongside unit testing. When at least one of the postconditions tests, because it tries to generalize them, but on a of a property has failed, then the test fails, the long term it may strive to replace unit testing for the entire generic test completes and the actions taken VMXL4 microkernel API. during the test are printed alongside their input. The second situation in which a test fails is when its state 4.1. Implementation Starting Point becomes inconsistent, meaning that no property has all of its preconditions passing and therefore no The implementation is based on the open source future action can be taken. When a test fails, the project developed by Pennebaker (2012). It is a basic programmer sees all the randomly generated data framework, supporting only two features: random used by the test and this facilitates easier debugging. data generation and one property per test, which was run for a predefined number of times. A part Properties are divided in two categories: normal of the implementation is not really usable, because properties and cleanup properties. Normal prop- the programmer who uses the framework must know erties are placeholders for actions that the sys- the size of the generated types and create tests tem may take anytime, provided the preconditions accordingly, which is error-prone. The only part are satisfied. Cleanup properties are used to end which we partially used is the test data generation tests and to free allocated resources. Every test component. must have at least one cleanup property. If a test does not have allocated resources, QC provides the The framework is implemented in the C program- empty clean property macro for an empty property, ming language because it was the most convenient whose only purpose is to end the test. Although option taking into consideration the testing environ- most of the time only one cleanup property will ment. Porting a new language environment can be be used for a generic test, having multiple cleanup very complicated, because the native environment properties may be useful in some situations. One offered by a microkernel is very low-level. Moreover, can use fine-grained cleanup properties if the system implementing a POSIX environment is equivalent can have many internal states. This makes the code with the implementation of an entire operating sys- cleaner and in a system with many generic tests, the tem. Also, because the API had already been written probability to reuse cleanup properties is bigger if in C, there is no need for further linking between they are fine-grained. different languages. 4 https://www.scalacheck.org/ A higher level design of QC is shown in Figure 2. The programmer must call QC with an array of normal properties and an array of cleanup properties, as previously discussed. To generate random input and 1RUPDO 4&)UDPHZRUN A QC generator consists of 2 callbacks: one to 3URSHUWLHV generate the data and the other to print the *URXS 6HHG 9HUERVLW\OHYHO data, as the C printf function needs different formats depending on the printed type. Because of 7\SHRIVWDWLVWLFV 1XPEHURIWHVWV that, the QC equivalent of a generator is struct 3URS  generator printer. 0LQLPXPQXPEHURISURSHUWLHVSHUWHVW QC offers a set of predefined generators for C 3URS basic data types, such as int and char, and also  for bool, string (stored as a char dynamic array) 4&7HVWV and generic arrays. Moreover, a user can write his  own generators or printers and use them for his  properties.  In order to generate arrays, only the basic type generator is needed, because QC offers a wrapper &OHDQXS3URSHUWLHV*URXS which automatically generates new array types. The array type can have fixed or random size in a given 3URS 3URS range, depending on the user needs. All generated      arrays are dynamically allocated and their memory is freed after their associated property ends. This avoids out of memory errors for big tests with many Figure 2: QC design generated arrays, but can introduce subtle bugs if the user forgets to copy the content of the array in case he needs it after the property ends. randomly pick properties, QC uses a seed. When a test fails, the programmer will want to reproduce the Sometimes basic types may need additional features exact same sequence of properties and inputs to test such as a maximum or minimum value. QC offers two the fix for the bug. Because the random generation is solutions for this. The first one is that miscellaneous deterministic given the seed, QC shows it for every parameters can be added to the generators, in generic test so the programmer can use that seed order to modify the generated value to match the if he wants to reproduce the tests. Otherwise, QC requirements. The second solution is to change and generates a random seed to assure random tests update the generated values from the property code. and a good test coverage. Both solutions are acceptable for code readability, but in general cases the first option should be used, QC will generate a fixed number of tests, previously because it’s reusable and only the parameters will be given by the user. Another available option is the changed. verbosity level for generic tests. The user can see the sequence used by every test or only by failing All generated data for a property is stored in a tests. Viewing the sequence used by every test can dynamically allocated array with the size in bytes be useful to improve the generic test and its test equal to the maximum number of arguments of a coverage. property multiplied by the maximum size in bytes of an argument type. This approach solves the problem There may be cases when tests will end prematurely, with the variable number of property arguments and after using only a few properties, because QC may their different types. The value of the generated data choose and use a cleanup property whenever its is obtained in the property and the user must only preconditions are satisfied. To mitigate this, the user know the data type and the index of the argument, chooses the minimum number of properties that something that he had already defined in the state must be used during a test. machine test specification. The last parameter from Figure 2 represents the type 4.4. Statistics of statistics shown at the end of the generic test. QC supports two types of statistics for every generic test: In order to measure various metrics, QC offers user defined and automatically generated. The user the possibility to attach user defined statistics to a can choose to see both categories, only one or none. property. After a property ends successfully, each of its statistics callbacks is called and the metrics are 4.3. Generators updated. This can help the user to investigate bugs and also measure the test coverage. An example of As previously mentioned, generators are the this logging category is shown in Listing 7. callbacks that randomly produce the input data. • • • • By default, QC logs statistics regarding properties and their sequence. For every property, QC logs the 3URSHUW\ number of total calls, the number of starting test property calls and for every property how many times *HQHUDWRU 6WDWLVWLF it followed the current property. An example of this 3ULQWHU type of logging is shown in Listing 8. The default *HQHUDWRU logging done by QC can be very useful to detect 6WDWLVWLF 3ULQWHU 3URSHUW\ preconditions bugs and see if the tests are surfacing  LQIR  the desired states.     The user decides if he wants to see any of the two *HQHUDWRU statistics category when the QC framework is called 6WDWLVWLFM 3ULQWHUL to generate and validate tests. 3UHFRQGLWLRQV 4.5. Properties, Preconditions and Postconditions Figure 3: Property info callbacks Since QC supports stateful system testing, using a property requires the following steps: testing As can be seen in Figure 3, QC properties are preconditions, getting the values for the randomly composed of multiple callbacks, stored in a structure generated data, applying actions and testing named property info. We need an array of generators postconditions. for the property input and another array of user The preconditions are optional but if they are defined statistics to gather various data. On the missing, the property can be always chosen by the other side, we need a callback for preconditions framework as the next part of the test. Preconditions and a callback for the property itself, to make the are implemented as a callback, differently from API calls and test the postconditions. Having all the property callback. Because the preconditions of those callbacks, different components of generic depend only on the internal state, not on the tests become easier to integrate with each other. generated data, it is better to obtain the new struct p r o p e r t y i n f o { data only if the property can be applied, avoiding / ∗ callback f o r the property ∗ / generation of useless data, which will be replaced prop f u n c t i o n ; afterwards. Therefore, preconditions must be tested before the data generation step and this can be / ∗ d i s p l a y i n g name ∗ / achieved by having another callback, associated with char const ∗ const name ; a property. This approach has another benefit: some preconditions are used by multiple properties and /∗ array of generators ∗/ having them as functions gives better reusability. If s t r u c t g e n e r a t o r p r i n t e r ∗gp ; a property does not have any preconditions, their callback will be NULL. To address any possible usage, / ∗ number o f g e n e r a t o r s ∗ / preconditions can be used from inside the property int gp size ; too, but this is not a good practice, as explained above. /∗ preconditions callback ∗/ p r e c o n d i t i o n prec ; Actions are the main content of properties, because they change the state of the system and their side /∗ array of s t a t i s t i c s callbacks ∗/ effects are verified by the postconditions. Actions struct u s e r s t a t i s t i c ∗ stats ; can be interleaved with their postconditions, which are obtained from the formal specification of the / ∗ number o f s t a t i s t i c s c a l l b a c k s ∗ / API. As opposed to preconditions, postconditions int stats size ; are located in their corresponding property callback, }; because they depend on the generated data and we do not obtain a performance improvement if we have Listing 3: Struct property info them in separate callbacks. Moreover, if the property contains multiple actions, then it is recommended to In QC’s implementation, property descriptions and check the postconditions for an action or a group of callbacks are contained by the property info actions as soon as possible, in order to have good structure, as shown in Listing 3. In addition to what code readability. was previously discussed, the name field assigns a • • • • descriptive name to the property and is used for the prop fail if and prop fail unless, wrappers verbosity option QC INFO or for failing tests. similar to Check’s fail if and fail unless. 4.6. QC test logic 5. QC EVALUATION AND TESTING Having all the previously discussed elements, QC can generate and run tests. Figure 4 shows a state This section describes evaluation, results and machine with the actions taken by QC during a test. implications, while the framework is still under Until a test fails or the required number of tests have development. To evaluate the performance of the QC been run, the framework tries to falsify the generic framework, its impact on the test coverage and code test by finding a failing test. size will be detailed. / ∗ normal p r o p e r t i e s ∗ / Starting a test, QC chooses a property, checks struct p r o p e r t y i n f o p [ ] = { its preconditions (should they exist) and, based on {init property , ” i n i t ” , the result, picks another property or continues with ( gp array ){ q c u i n t } , 1 , the current one. If the preconditions have passed, q is not initialized , QC generates test data, executes the actions and ( s t a t s a r r a y ) { q u e u e s i z e s t a t } , 1} , the postconditions are checked. If any of the { dequeue property , ” dequeue ” , postconditions fails, the testing is over, because QC ( gp array ){} , 0 , falsified a sequence of properties. Otherwise, the q is initialized , statistics are updated and if the property is from NULL , 0} , the cleanup group, the current test completes and { enqueue property , ” enqueue ” , another test starts; if the property is from the normal ( gp array ){ q c i n t } , 1 , group, the test continues and another property is q is initialized , chosen. ( s t a t s a r r a y ) { e l e m e n t s i g n s t a t } , 1} 4.7. Pseudorandom number generator }; QC has a random module which currently supports s t r u c t p r o p e r t y g r o u p normal group = { two implementations: the POSIX rand function . prop = p , . s i z e = 3 and the Mersenne Twister PRNG. The default }; implementation is Mersenne Twister (presented in Matsumoto and Nishimura (1998)), because it / ∗ cleanup p r o p e r t i e s ∗ / provides better data distribution than rand and struct p r o p e r t y i n f o clean p [ ] = { always has the same output for a given seed, on { clear property , ” clear ” , 32 bits, in contrast with rand, whose result may vary ( gp array ){} , 0 , depending on the architecture. q is initialized , NULL , 0} 4.8. VMXL4 Influence over QC }; Internally QC uses a seed for randomizing the struct property group clean group = { test data generation and the chosen property at . prop = clean p , . s i z e = 1 every step of a test. Because the VMXL4 native }; environment is under ongoing development and some POSIX functions (e.g. rand) are not yet qc for all ( implemented, inside the testing environment the / ∗ p r o p e r t y groups ∗ / seed is actually a numerical value obtained from normal group , clean group , a hardware timer provided by the development / ∗ minimum p r o p e r t i e s ∗ / platform. However, the framework does not depend 5, on a specific platform and is portable, requiring only /∗ verbosity level ∗/ POSIX functionality. QC ERROR, / ∗ number o f t e s t s ∗ / The VMXL4 API is currently being tested using 1000 , the Check Unit Testing Framework for C. In order /∗ s t a t i s t i c s level ∗/ to be as easy as possible to use and because QC SHOW STATS unit tests usually need little changes to become ); properties, the QC interface has been designed to have some similarities with the Check framework. Listing 4: QC initialization and calling to test a circular For that reason, postconditions can be tested using queue library API 7HVWSDVVHV