A Property Language for the Specification of Hardware-Dependent Embedded System Software

This paper introduces a new property language for describing the behavior of low-level hardware-dependent software. The design of the language is motivated by the industrial success of property languages for hardware verification by simulation and formal techniques. The new language is constructed to concisely capture the timed behavior of the interactions between software and hardware by means of sequences. In this work we present how the proposed verification language can be used to perform formal verification based on a computational model called program netlist. We show how the sequence model of the language is synthesized and combined with the program netlist so that a unified formula for a decision procedure, e.g., a SAT solver, can be constructed. Furthermore, a method for coverage analysis of property sets is introduced. The coverage criterion we propose determines whether or not the property set completely describes the input/output functional behavior of a program. The paper presents a case study showing how to use the proposed property language in order to specify an industrial implementation of a LIN (Local Interconnect Network) bus driver.