Scenario Patterns and Trace-Based Temporal Verification of Reactive Embedded Systems

This paper introduces a formal scenario description and a set of patterns for timing constraints that can assist designers with specifying and testing reactive embedded systems. The description of a scenario may be complemented by activities, which specify input-output relations and maximum response times. We also introduce a monitor that have been implemented to verify scenarios and activities on a time stamped trace of system variables, both on lab tests and on field operation. Therefore using our monitor spares designers the time of developing additional software for system tests. Moreover, since verification routines are completely defined in the monitor, once the scenario descriptions are completed, it is possible to determine the maximum time required to process a scenario per trace line. This time is a function of the numbers of variables and timing constraints under scrutiny. In our experiments, we have used the requirements of three automotive applications to assess the expressiveness of our scenarios. Synthetic traces have been generated to measure the performance of our monitor with the formal scenarios written for a set of requirements. On experiments with our monitor running on the FreescaleTM micro controller 9S12XDP512, we measured the maximum processing time per trace line for scenarios with different numbers of variables and timing constraints.