The goal of HITECS model checking is to show the well-behavedness of HITECS specifications based on our requirements to detect uncertainties. To do so, the requirements must first be specified in terms of assertions. The effectiveness of model checking highly depends on the precision and quality of the underlying assertions. To address this difficulty, we provide guidelines to help test engineers specify precise well-behavedness assertions for HiL test cases and place these assertions in appropriate locations within HITECS specifications.

Having defined our guidelines for assertion specification, we now describe the steps of HITECS model checking in the figure. The ``HITECS into JAVA translation'' step produces the Java translation of HITECS specifications. This step converts HITECS assertions into Java assertions and the unknown variables are replaced with random-number generators. The second step consists of adding the negations of the assertions in Java in order to check their well-behavedness. To check whether an assertion holds, we run a well known symbolic model checker, Java PathFinder. A property is proved when the assertion and its negation are reported as True and refuted when one of the assertions is reported as False. In addition, a property is uncertain when the assertion and its negation are both reported as False by Java PathFinder.

The goal of HITECS simulation is to estimate execution times of HiL test cases at an early stage without having to exercise them against the hardware. The figure above describes of HITECS simulation, which starts with translating HITECS into Java. This step excludes the simulation annotations for the code and translates the annotation semantics to Java specifications. The latter is executed using the ``Execute java'' step in order to generate execution traces for each annotation inserted in HITECS.

The next step consists of analyzing the traces by computing the simulation results based on the output traces generated by ``Execute Java'' step. ``Analyze traces'' step includes some pre-defined functions aggregating these outputs. Specifically, for each annotation in the input HITECS specifications, engineers need to select an aggregator function from the pre-defined ones. For each trace, the aggregator computes the execution times generated by calls to the annotation semantics routine. HITECS simulation represents a distribution of the execution time values of the HiL test case under analysis obtained based on severals runs of the test case.