A monitoring approach to facilitate run-time verification of software in deeply embedded systems

With embedded systems growing in hardware and software complexity, it is becoming increasingly difficult to avoid failures, despite costly design and testing efforts. Monitoring the behaviour of an embedded system's software is useful both during the product testing phase and in the field environment and can contribute to confidence in the overall system. Run-time verification combines monitoring with formal methods by checking specified rules against run-time observations. Embedded systems pose some problems for run-time verification, as their limited resources may preclude internal monitoring features and their self-contained design may inhibit sufficient observation of the software execution by an external monitor. The main aim of the research outlined in this thesis is to investigate the feasibility of using run-time verification as a monitoring approach for software executing in an embedded system. An experimental evaluation framework is described that supports the study of this approach. The embedded system comprises a Java Optimised Processor (JOP) soft processor, instantiated in the fabric of an FPGA (field programmable gate array). The experimental system employs the Java-MaC (Java Monitoring and Checking) run-time verification method, arranged to indirectly monitor the run-time behaviour of a software application executing on JOP. The experimental framework successfully allows run-time verification of a software application executing on the FPGA. A case study is presented that demonstrates that the monitoring approach is sufficient to observe a number of parameters used in an example ‘railroad crossing’ run-time verification scenario. A second case study aims to verify that a set of tasks scheduled under the rate-monotonic algorithm is scheduled at run time as predicted by static offline analysis. The results of the case studies provide detail on the potential and limitations of the monitoring arrangement. The gathered data is used to support recommendations for monitoring embedded systems, presented at the conclusion of this thesis.