Efficient Runtime Verification of Energy Properties within Hardware / Software Co-Design

The most reliable systems within the aerospace domain continually leverage formal methods to prove system correctness against project requirements. Most systems verify value-domain requirements to ensure functional correctness of the application. This approach only examines one of the key domains within which to apply formal methods. Aerospace applications contain many constrained resources that when over-utilised can lead to mission failure. One such constraint is energy, as space missions use minimal energy stores to power and maintain normal operating functions. In this paper, we extend formal methods to verify energy within the process of Hardware / Software Co-Design. Particularly, we focus on developing applications in FPGAs, while measuring energy usage at runtime. We combine this engineering data with formal methods and our requirements specified in temporal logics to formally verify energy constraints. Our approach is runtime verification in the purest sense, as our system measures energy by executing all possible branches of the user's logic. Our approach is compatible with existing methods in continuous verification and agile development.